f(f(s(x), 0), f(y, z)) → f(f(y, z), f(y, s(z)))
f(f(s(x), s(y)), f(z, w)) → f(f(x, y), f(z, w))
↳ QTRS
↳ DependencyPairsProof
f(f(s(x), 0), f(y, z)) → f(f(y, z), f(y, s(z)))
f(f(s(x), s(y)), f(z, w)) → f(f(x, y), f(z, w))
F(f(s(x), s(y)), f(z, w)) → F(x, y)
F(f(s(x), 0), f(y, z)) → F(y, s(z))
F(f(s(x), s(y)), f(z, w)) → F(f(x, y), f(z, w))
F(f(s(x), 0), f(y, z)) → F(f(y, z), f(y, s(z)))
f(f(s(x), 0), f(y, z)) → f(f(y, z), f(y, s(z)))
f(f(s(x), s(y)), f(z, w)) → f(f(x, y), f(z, w))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
F(f(s(x), s(y)), f(z, w)) → F(x, y)
F(f(s(x), 0), f(y, z)) → F(y, s(z))
F(f(s(x), s(y)), f(z, w)) → F(f(x, y), f(z, w))
F(f(s(x), 0), f(y, z)) → F(f(y, z), f(y, s(z)))
f(f(s(x), 0), f(y, z)) → f(f(y, z), f(y, s(z)))
f(f(s(x), s(y)), f(z, w)) → f(f(x, y), f(z, w))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ ForwardInstantiation
F(f(s(x), s(y)), f(z, w)) → F(x, y)
F(f(s(x), s(y)), f(z, w)) → F(f(x, y), f(z, w))
F(f(s(x), 0), f(y, z)) → F(f(y, z), f(y, s(z)))
f(f(s(x), 0), f(y, z)) → f(f(y, z), f(y, s(z)))
f(f(s(x), s(y)), f(z, w)) → f(f(x, y), f(z, w))
F(f(s(s(y_0)), s(0)), f(x2, x3)) → F(f(s(y_0), 0), f(x2, x3))
F(f(s(s(y_0)), s(s(y_1))), f(x2, x3)) → F(f(s(y_0), s(y_1)), f(x2, x3))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ ForwardInstantiation
F(f(s(s(y_0)), s(0)), f(x2, x3)) → F(f(s(y_0), 0), f(x2, x3))
F(f(s(x), s(y)), f(z, w)) → F(x, y)
F(f(s(x), 0), f(y, z)) → F(f(y, z), f(y, s(z)))
F(f(s(s(y_0)), s(s(y_1))), f(x2, x3)) → F(f(s(y_0), s(y_1)), f(x2, x3))
f(f(s(x), 0), f(y, z)) → f(f(y, z), f(y, s(z)))
f(f(s(x), s(y)), f(z, w)) → f(f(x, y), f(z, w))
F(f(s(x0), 0), f(s(s(y_0)), s(0))) → F(f(s(s(y_0)), s(0)), f(s(s(y_0)), s(s(0))))
F(f(s(x0), 0), f(s(y_0), s(y_1))) → F(f(s(y_0), s(y_1)), f(s(y_0), s(s(y_1))))
F(f(s(x0), 0), f(s(s(y_0)), s(s(y_1)))) → F(f(s(s(y_0)), s(s(y_1))), f(s(s(y_0)), s(s(s(y_1)))))
F(f(s(x0), 0), f(s(y_0), 0)) → F(f(s(y_0), 0), f(s(y_0), s(0)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ ForwardInstantiation
F(f(s(x0), 0), f(s(y_0), s(y_1))) → F(f(s(y_0), s(y_1)), f(s(y_0), s(s(y_1))))
F(f(s(x0), 0), f(s(s(y_0)), s(0))) → F(f(s(s(y_0)), s(0)), f(s(s(y_0)), s(s(0))))
F(f(s(s(y_0)), s(0)), f(x2, x3)) → F(f(s(y_0), 0), f(x2, x3))
F(f(s(x), s(y)), f(z, w)) → F(x, y)
F(f(s(x0), 0), f(s(s(y_0)), s(s(y_1)))) → F(f(s(s(y_0)), s(s(y_1))), f(s(s(y_0)), s(s(s(y_1)))))
F(f(s(x0), 0), f(s(y_0), 0)) → F(f(s(y_0), 0), f(s(y_0), s(0)))
F(f(s(s(y_0)), s(s(y_1))), f(x2, x3)) → F(f(s(y_0), s(y_1)), f(x2, x3))
f(f(s(x), 0), f(y, z)) → f(f(y, z), f(y, s(z)))
f(f(s(x), s(y)), f(z, w)) → f(f(x, y), f(z, w))
F(f(s(f(s(y_0), 0)), s(f(s(s(y_1)), s(s(y_2))))), f(x2, x3)) → F(f(s(y_0), 0), f(s(s(y_1)), s(s(y_2))))
F(f(s(f(s(y_0), 0)), s(f(s(s(y_1)), s(0)))), f(x2, x3)) → F(f(s(y_0), 0), f(s(s(y_1)), s(0)))
F(f(s(f(s(y_0), s(y_1))), s(x1)), f(x2, x3)) → F(f(s(y_0), s(y_1)), x1)
F(f(s(f(s(y_0), 0)), s(f(s(y_1), 0))), f(x2, x3)) → F(f(s(y_0), 0), f(s(y_1), 0))
F(f(s(f(s(s(y_0)), s(s(y_1)))), s(x1)), f(x2, x3)) → F(f(s(s(y_0)), s(s(y_1))), x1)
F(f(s(f(s(s(y_0)), s(0))), s(x1)), f(x2, x3)) → F(f(s(s(y_0)), s(0)), x1)
F(f(s(f(s(y_0), 0)), s(f(s(y_1), s(y_2)))), f(x2, x3)) → F(f(s(y_0), 0), f(s(y_1), s(y_2)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ SemLabProof
↳ SemLabProof2
F(f(s(s(y_0)), s(0)), f(x2, x3)) → F(f(s(y_0), 0), f(x2, x3))
F(f(s(f(s(y_0), 0)), s(f(s(s(y_1)), s(s(y_2))))), f(x2, x3)) → F(f(s(y_0), 0), f(s(s(y_1)), s(s(y_2))))
F(f(s(f(s(y_0), 0)), s(f(s(s(y_1)), s(0)))), f(x2, x3)) → F(f(s(y_0), 0), f(s(s(y_1)), s(0)))
F(f(s(f(s(y_0), s(y_1))), s(x1)), f(x2, x3)) → F(f(s(y_0), s(y_1)), x1)
F(f(s(f(s(s(y_0)), s(s(y_1)))), s(x1)), f(x2, x3)) → F(f(s(s(y_0)), s(s(y_1))), x1)
F(f(s(f(s(y_0), 0)), s(f(s(y_1), s(y_2)))), f(x2, x3)) → F(f(s(y_0), 0), f(s(y_1), s(y_2)))
F(f(s(x0), 0), f(s(y_0), s(y_1))) → F(f(s(y_0), s(y_1)), f(s(y_0), s(s(y_1))))
F(f(s(x0), 0), f(s(s(y_0)), s(0))) → F(f(s(s(y_0)), s(0)), f(s(s(y_0)), s(s(0))))
F(f(s(x0), 0), f(s(s(y_0)), s(s(y_1)))) → F(f(s(s(y_0)), s(s(y_1))), f(s(s(y_0)), s(s(s(y_1)))))
F(f(s(x0), 0), f(s(y_0), 0)) → F(f(s(y_0), 0), f(s(y_0), s(0)))
F(f(s(f(s(y_0), 0)), s(f(s(y_1), 0))), f(x2, x3)) → F(f(s(y_0), 0), f(s(y_1), 0))
F(f(s(s(y_0)), s(s(y_1))), f(x2, x3)) → F(f(s(y_0), s(y_1)), f(x2, x3))
F(f(s(f(s(s(y_0)), s(0))), s(x1)), f(x2, x3)) → F(f(s(s(y_0)), s(0)), x1)
f(f(s(x), 0), f(y, z)) → f(f(y, z), f(y, s(z)))
f(f(s(x), s(y)), f(z, w)) → f(f(x, y), f(z, w))
F.0-0(f.0-0(s.0(f.0-1(s.0(y_0), 0.)), s.0(f.0-1(s.0(s.0(y_1)), s.1(0.)))), f.1-0(x2, x3)) → F.0-0(f.0-1(s.0(y_0), 0.), f.0-1(s.0(s.0(y_1)), s.1(0.)))
F.0-0(f.0-0(s.0(f.1-1(s.1(s.1(y_0)), s.1(0.))), s.0(x1)), f.1-1(x2, x3)) → F.0-0(f.1-1(s.1(s.1(y_0)), s.1(0.)), x1)
F.0-0(f.0-0(s.0(f.0-1(s.0(y_0), 0.)), s.0(f.0-1(s.0(y_1), 0.))), f.0-1(x2, x3)) → F.0-0(f.0-1(s.0(y_0), 0.), f.0-1(s.0(y_1), 0.))
F.0-0(f.0-0(s.0(f.0-1(s.0(y_0), 0.)), s.0(f.0-0(s.0(y_1), s.0(y_2)))), f.1-1(x2, x3)) → F.0-0(f.0-1(s.0(y_0), 0.), f.0-0(s.0(y_1), s.0(y_2)))
F.0-0(f.0-0(s.0(f.0-1(s.0(y_0), 0.)), s.0(f.0-1(s.0(s.0(y_1)), s.1(0.)))), f.0-1(x2, x3)) → F.0-0(f.0-1(s.0(y_0), 0.), f.0-1(s.0(s.0(y_1)), s.1(0.)))
F.0-0(f.0-0(s.0(f.0-1(s.0(y_0), 0.)), s.0(f.1-0(s.1(s.1(y_1)), s.0(s.0(y_2))))), f.1-0(x2, x3)) → F.0-0(f.0-1(s.0(y_0), 0.), f.1-0(s.1(s.1(y_1)), s.0(s.0(y_2))))
F.0-0(f.0-0(s.0(f.1-0(s.1(y_0), s.0(y_1))), s.0(x1)), f.0-0(x2, x3)) → F.0-0(f.1-0(s.1(y_0), s.0(y_1)), x1)
F.0-0(f.0-0(s.0(f.1-1(s.1(y_0), 0.)), s.0(f.0-1(s.0(y_1), s.1(y_2)))), f.0-0(x2, x3)) → F.0-0(f.1-1(s.1(y_0), 0.), f.0-1(s.0(y_1), s.1(y_2)))
F.0-0(f.0-0(s.0(f.0-1(s.0(y_0), 0.)), s.0(f.1-1(s.1(y_1), s.1(y_2)))), f.0-0(x2, x3)) → F.0-0(f.0-1(s.0(y_0), 0.), f.1-1(s.1(y_1), s.1(y_2)))
F.0-0(f.0-1(s.0(s.0(y_0)), s.1(0.)), f.0-0(x2, x3)) → F.0-0(f.0-1(s.0(y_0), 0.), f.0-0(x2, x3))
F.0-0(f.0-0(s.0(f.0-1(s.0(y_0), 0.)), s.0(f.0-0(s.0(y_1), s.0(y_2)))), f.1-0(x2, x3)) → F.0-0(f.0-1(s.0(y_0), 0.), f.0-0(s.0(y_1), s.0(y_2)))
F.0-0(f.0-1(s.0(f.1-0(s.1(y_0), s.0(y_1))), s.1(x1)), f.1-0(x2, x3)) → F.0-1(f.1-0(s.1(y_0), s.0(y_1)), x1)
F.0-0(f.0-0(s.0(f.0-1(s.0(y_0), 0.)), s.0(f.1-1(s.1(y_1), 0.))), f.1-0(x2, x3)) → F.0-0(f.0-1(s.0(y_0), 0.), f.1-1(s.1(y_1), 0.))
F.0-0(f.0-0(s.0(f.1-1(s.1(y_0), 0.)), s.0(f.0-1(s.0(y_1), 0.))), f.1-0(x2, x3)) → F.0-0(f.1-1(s.1(y_0), 0.), f.0-1(s.0(y_1), 0.))
F.0-0(f.0-0(s.0(f.0-1(s.0(y_0), 0.)), s.0(f.0-0(s.0(y_1), s.0(y_2)))), f.0-0(x2, x3)) → F.0-0(f.0-1(s.0(y_0), 0.), f.0-0(s.0(y_1), s.0(y_2)))
F.0-0(f.0-0(s.0(f.0-1(s.0(y_0), 0.)), s.0(f.0-1(s.0(y_1), s.1(y_2)))), f.0-0(x2, x3)) → F.0-0(f.0-1(s.0(y_0), 0.), f.0-1(s.0(y_1), s.1(y_2)))
F.0-0(f.0-0(s.0(f.1-1(s.1(y_0), 0.)), s.0(f.1-1(s.1(s.1(y_1)), s.1(s.1(y_2))))), f.1-0(x2, x3)) → F.0-0(f.1-1(s.1(y_0), 0.), f.1-1(s.1(s.1(y_1)), s.1(s.1(y_2))))
F.0-0(f.1-1(s.1(x0), 0.), f.1-0(s.1(s.1(y_0)), s.0(s.0(y_1)))) → F.0-0(f.1-0(s.1(s.1(y_0)), s.0(s.0(y_1))), f.1-0(s.1(s.1(y_0)), s.0(s.0(s.0(y_1)))))
F.0-0(f.0-0(s.0(f.0-1(s.0(y_0), 0.)), s.0(f.1-1(s.1(s.1(y_1)), s.1(0.)))), f.0-1(x2, x3)) → F.0-0(f.0-1(s.0(y_0), 0.), f.1-1(s.1(s.1(y_1)), s.1(0.)))
F.0-0(f.0-0(s.0(f.0-1(s.0(y_0), 0.)), s.0(f.0-1(s.0(y_1), s.1(y_2)))), f.1-1(x2, x3)) → F.0-0(f.0-1(s.0(y_0), 0.), f.0-1(s.0(y_1), s.1(y_2)))
F.0-0(f.0-0(s.0(f.1-1(s.1(y_0), 0.)), s.0(f.1-1(s.1(s.1(y_1)), s.1(0.)))), f.0-0(x2, x3)) → F.0-0(f.1-1(s.1(y_0), 0.), f.1-1(s.1(s.1(y_1)), s.1(0.)))
F.0-0(f.0-0(s.0(f.1-1(s.1(y_0), 0.)), s.0(f.0-1(s.0(y_1), s.1(y_2)))), f.1-0(x2, x3)) → F.0-0(f.1-1(s.1(y_0), 0.), f.0-1(s.0(y_1), s.1(y_2)))
F.0-0(f.0-0(s.0(f.0-1(s.0(y_0), 0.)), s.0(f.1-1(s.1(y_1), s.1(y_2)))), f.1-0(x2, x3)) → F.0-0(f.0-1(s.0(y_0), 0.), f.1-1(s.1(y_1), s.1(y_2)))
F.0-0(f.0-0(s.0(f.0-1(s.0(y_0), s.1(y_1))), s.0(x1)), f.0-0(x2, x3)) → F.0-0(f.0-1(s.0(y_0), s.1(y_1)), x1)
F.0-0(f.1-1(s.1(s.1(y_0)), s.1(0.)), f.1-1(x2, x3)) → F.0-0(f.1-1(s.1(y_0), 0.), f.1-1(x2, x3))
F.0-0(f.0-0(s.0(f.1-1(s.1(y_0), 0.)), s.0(f.1-1(s.1(s.1(y_1)), s.1(s.1(y_2))))), f.1-1(x2, x3)) → F.0-0(f.1-1(s.1(y_0), 0.), f.1-1(s.1(s.1(y_1)), s.1(s.1(y_2))))
F.0-0(f.0-0(s.0(f.0-1(s.0(y_0), 0.)), s.0(f.1-1(s.1(s.1(y_1)), s.1(0.)))), f.1-0(x2, x3)) → F.0-0(f.0-1(s.0(y_0), 0.), f.1-1(s.1(s.1(y_1)), s.1(0.)))
F.0-0(f.0-1(s.0(x0), 0.), f.1-1(s.1(s.1(y_0)), s.1(s.1(y_1)))) → F.0-0(f.1-1(s.1(s.1(y_0)), s.1(s.1(y_1))), f.1-1(s.1(s.1(y_0)), s.1(s.1(s.1(y_1)))))
F.0-0(f.0-0(s.0(f.0-1(s.0(s.0(y_0)), s.1(0.))), s.0(x1)), f.1-0(x2, x3)) → F.0-0(f.0-1(s.0(s.0(y_0)), s.1(0.)), x1)
F.0-0(f.0-0(s.0(f.1-1(s.1(s.1(y_0)), s.1(0.))), s.0(x1)), f.1-0(x2, x3)) → F.0-0(f.1-1(s.1(s.1(y_0)), s.1(0.)), x1)
F.0-0(f.0-0(s.0(f.1-1(s.1(y_0), 0.)), s.0(f.0-0(s.0(y_1), s.0(y_2)))), f.0-0(x2, x3)) → F.0-0(f.1-1(s.1(y_0), 0.), f.0-0(s.0(y_1), s.0(y_2)))
F.0-0(f.0-0(s.0(f.0-1(s.0(y_0), 0.)), s.0(f.1-0(s.1(y_1), s.0(y_2)))), f.0-0(x2, x3)) → F.0-0(f.0-1(s.0(y_0), 0.), f.1-0(s.1(y_1), s.0(y_2)))
F.0-0(f.0-0(s.0(f.0-1(s.0(y_0), 0.)), s.0(f.0-1(s.0(s.0(y_1)), s.1(s.1(y_2))))), f.1-0(x2, x3)) → F.0-0(f.0-1(s.0(y_0), 0.), f.0-1(s.0(s.0(y_1)), s.1(s.1(y_2))))
F.0-0(f.1-1(s.1(x0), 0.), f.1-1(s.1(y_0), s.1(y_1))) → F.0-0(f.1-1(s.1(y_0), s.1(y_1)), f.1-1(s.1(y_0), s.1(s.1(y_1))))
F.0-0(f.0-1(s.0(f.0-0(s.0(s.0(y_0)), s.0(s.0(y_1)))), s.1(x1)), f.0-1(x2, x3)) → F.0-1(f.0-0(s.0(s.0(y_0)), s.0(s.0(y_1))), x1)
F.0-0(f.0-0(s.0(f.1-0(s.1(y_0), s.0(y_1))), s.0(x1)), f.1-1(x2, x3)) → F.0-0(f.1-0(s.1(y_0), s.0(y_1)), x1)
F.0-0(f.0-0(s.0(f.1-1(s.1(y_0), 0.)), s.0(f.1-1(s.1(y_1), 0.))), f.0-1(x2, x3)) → F.0-0(f.1-1(s.1(y_0), 0.), f.1-1(s.1(y_1), 0.))
F.0-0(f.0-0(s.0(f.0-1(s.0(y_0), 0.)), s.0(f.0-1(s.0(y_1), s.1(y_2)))), f.1-0(x2, x3)) → F.0-0(f.0-1(s.0(y_0), 0.), f.0-1(s.0(y_1), s.1(y_2)))
F.0-0(f.0-0(s.0(f.0-1(s.0(y_0), s.1(y_1))), s.0(x1)), f.1-0(x2, x3)) → F.0-0(f.0-1(s.0(y_0), s.1(y_1)), x1)
F.0-0(f.0-0(s.0(f.0-1(s.0(y_0), 0.)), s.0(f.1-1(s.1(s.1(y_1)), s.1(s.1(y_2))))), f.0-0(x2, x3)) → F.0-0(f.0-1(s.0(y_0), 0.), f.1-1(s.1(s.1(y_1)), s.1(s.1(y_2))))
F.0-0(f.0-0(s.0(f.1-0(s.1(y_0), s.0(y_1))), s.0(x1)), f.0-1(x2, x3)) → F.0-0(f.1-0(s.1(y_0), s.0(y_1)), x1)
F.0-0(f.0-0(s.0(f.0-1(s.0(y_0), 0.)), s.0(f.1-0(s.1(s.1(y_1)), s.0(s.0(y_2))))), f.1-1(x2, x3)) → F.0-0(f.0-1(s.0(y_0), 0.), f.1-0(s.1(s.1(y_1)), s.0(s.0(y_2))))
F.0-0(f.0-1(s.0(f.0-0(s.0(y_0), s.0(y_1))), s.1(x1)), f.0-0(x2, x3)) → F.0-1(f.0-0(s.0(y_0), s.0(y_1)), x1)
F.0-0(f.0-0(s.0(f.1-0(s.1(s.1(y_0)), s.0(s.0(y_1)))), s.0(x1)), f.1-1(x2, x3)) → F.0-0(f.1-0(s.1(s.1(y_0)), s.0(s.0(y_1))), x1)
F.0-0(f.0-0(s.0(f.1-0(s.1(s.1(y_0)), s.0(s.0(y_1)))), s.0(x1)), f.1-0(x2, x3)) → F.0-0(f.1-0(s.1(s.1(y_0)), s.0(s.0(y_1))), x1)
F.0-0(f.0-1(s.0(f.1-0(s.1(s.1(y_0)), s.0(s.0(y_1)))), s.1(x1)), f.0-0(x2, x3)) → F.0-1(f.1-0(s.1(s.1(y_0)), s.0(s.0(y_1))), x1)
F.0-0(f.0-1(s.0(x0), 0.), f.1-1(s.1(y_0), s.1(y_1))) → F.0-0(f.1-1(s.1(y_0), s.1(y_1)), f.1-1(s.1(y_0), s.1(s.1(y_1))))
F.0-0(f.0-0(s.0(f.0-1(s.0(y_0), 0.)), s.0(f.1-1(s.1(s.1(y_1)), s.1(0.)))), f.1-1(x2, x3)) → F.0-0(f.0-1(s.0(y_0), 0.), f.1-1(s.1(s.1(y_1)), s.1(0.)))
F.0-0(f.0-0(s.0(f.0-1(s.0(y_0), 0.)), s.0(f.0-0(s.0(s.0(y_1)), s.0(s.0(y_2))))), f.0-1(x2, x3)) → F.0-0(f.0-1(s.0(y_0), 0.), f.0-0(s.0(s.0(y_1)), s.0(s.0(y_2))))
F.0-0(f.0-1(s.0(f.1-1(s.1(s.1(y_0)), s.1(0.))), s.1(x1)), f.1-0(x2, x3)) → F.0-1(f.1-1(s.1(s.1(y_0)), s.1(0.)), x1)
F.0-0(f.0-0(s.0(f.1-1(s.1(y_0), 0.)), s.0(f.0-1(s.0(s.0(y_1)), s.1(s.1(y_2))))), f.1-1(x2, x3)) → F.0-0(f.1-1(s.1(y_0), 0.), f.0-1(s.0(s.0(y_1)), s.1(s.1(y_2))))
F.0-0(f.1-1(s.1(x0), 0.), f.0-1(s.0(y_0), 0.)) → F.0-0(f.0-1(s.0(y_0), 0.), f.0-1(s.0(y_0), s.1(0.)))
F.0-0(f.0-0(s.0(f.1-1(s.1(y_0), 0.)), s.0(f.1-0(s.1(s.1(y_1)), s.0(s.0(y_2))))), f.1-1(x2, x3)) → F.0-0(f.1-1(s.1(y_0), 0.), f.1-0(s.1(s.1(y_1)), s.0(s.0(y_2))))
F.0-0(f.0-1(s.0(f.0-0(s.0(y_0), s.0(y_1))), s.1(x1)), f.1-0(x2, x3)) → F.0-1(f.0-0(s.0(y_0), s.0(y_1)), x1)
F.0-0(f.0-0(s.0(f.1-1(s.1(y_0), 0.)), s.0(f.1-0(s.1(s.1(y_1)), s.0(s.0(y_2))))), f.0-1(x2, x3)) → F.0-0(f.1-1(s.1(y_0), 0.), f.1-0(s.1(s.1(y_1)), s.0(s.0(y_2))))
F.0-0(f.0-0(s.0(f.0-1(s.0(y_0), 0.)), s.0(f.0-0(s.0(s.0(y_1)), s.0(s.0(y_2))))), f.1-0(x2, x3)) → F.0-0(f.0-1(s.0(y_0), 0.), f.0-0(s.0(s.0(y_1)), s.0(s.0(y_2))))
F.0-0(f.0-1(s.0(f.0-1(s.0(s.0(y_0)), s.1(0.))), s.1(x1)), f.0-1(x2, x3)) → F.0-1(f.0-1(s.0(s.0(y_0)), s.1(0.)), x1)
F.0-0(f.1-1(s.1(x0), 0.), f.0-0(s.0(s.0(y_0)), s.0(s.0(y_1)))) → F.0-0(f.0-0(s.0(s.0(y_0)), s.0(s.0(y_1))), f.0-0(s.0(s.0(y_0)), s.0(s.0(s.0(y_1)))))
F.0-0(f.0-0(s.0(f.0-1(s.0(y_0), 0.)), s.0(f.0-1(s.0(s.0(y_1)), s.1(s.1(y_2))))), f.1-1(x2, x3)) → F.0-0(f.0-1(s.0(y_0), 0.), f.0-1(s.0(s.0(y_1)), s.1(s.1(y_2))))
F.0-0(f.0-1(s.0(f.1-1(s.1(s.1(y_0)), s.1(0.))), s.1(x1)), f.0-1(x2, x3)) → F.0-1(f.1-1(s.1(s.1(y_0)), s.1(0.)), x1)
F.0-0(f.0-0(s.0(f.1-1(s.1(y_0), 0.)), s.0(f.1-1(s.1(s.1(y_1)), s.1(s.1(y_2))))), f.0-0(x2, x3)) → F.0-0(f.1-1(s.1(y_0), 0.), f.1-1(s.1(s.1(y_1)), s.1(s.1(y_2))))
F.0-0(f.0-0(s.0(f.1-1(s.1(y_0), 0.)), s.0(f.0-1(s.0(s.0(y_1)), s.1(s.1(y_2))))), f.0-1(x2, x3)) → F.0-0(f.1-1(s.1(y_0), 0.), f.0-1(s.0(s.0(y_1)), s.1(s.1(y_2))))
F.0-0(f.0-1(s.0(x0), 0.), f.0-1(s.0(s.0(y_0)), s.1(s.1(y_1)))) → F.0-0(f.0-1(s.0(s.0(y_0)), s.1(s.1(y_1))), f.0-1(s.0(s.0(y_0)), s.1(s.1(s.1(y_1)))))
F.0-0(f.0-0(s.0(f.1-1(s.1(y_0), 0.)), s.0(f.1-0(s.1(y_1), s.0(y_2)))), f.0-0(x2, x3)) → F.0-0(f.1-1(s.1(y_0), 0.), f.1-0(s.1(y_1), s.0(y_2)))
F.0-0(f.0-0(s.0(f.0-1(s.0(s.0(y_0)), s.1(s.1(y_1)))), s.0(x1)), f.1-0(x2, x3)) → F.0-0(f.0-1(s.0(s.0(y_0)), s.1(s.1(y_1))), x1)
F.0-0(f.0-0(s.0(f.1-1(s.1(y_0), 0.)), s.0(f.1-0(s.1(y_1), s.0(y_2)))), f.1-1(x2, x3)) → F.0-0(f.1-1(s.1(y_0), 0.), f.1-0(s.1(y_1), s.0(y_2)))
F.0-0(f.0-0(s.0(f.1-1(s.1(y_0), 0.)), s.0(f.1-1(s.1(y_1), s.1(y_2)))), f.1-1(x2, x3)) → F.0-0(f.1-1(s.1(y_0), 0.), f.1-1(s.1(y_1), s.1(y_2)))
F.0-0(f.0-0(s.0(f.0-0(s.0(s.0(y_0)), s.0(s.0(y_1)))), s.0(x1)), f.0-1(x2, x3)) → F.0-0(f.0-0(s.0(s.0(y_0)), s.0(s.0(y_1))), x1)
F.0-0(f.0-0(s.0(f.1-1(s.1(y_0), 0.)), s.0(f.1-1(s.1(s.1(y_1)), s.1(0.)))), f.0-1(x2, x3)) → F.0-0(f.1-1(s.1(y_0), 0.), f.1-1(s.1(s.1(y_1)), s.1(0.)))
F.0-0(f.0-0(s.0(f.1-0(s.1(s.1(y_0)), s.0(s.0(y_1)))), s.0(x1)), f.0-1(x2, x3)) → F.0-0(f.1-0(s.1(s.1(y_0)), s.0(s.0(y_1))), x1)
F.0-0(f.0-0(s.0(f.1-1(s.1(y_0), 0.)), s.0(f.0-0(s.0(s.0(y_1)), s.0(s.0(y_2))))), f.1-1(x2, x3)) → F.0-0(f.1-1(s.1(y_0), 0.), f.0-0(s.0(s.0(y_1)), s.0(s.0(y_2))))
F.0-0(f.1-1(s.1(s.1(y_0)), s.1(s.1(y_1))), f.1-0(x2, x3)) → F.0-0(f.1-1(s.1(y_0), s.1(y_1)), f.1-0(x2, x3))
F.0-0(f.0-1(s.0(f.1-1(s.1(y_0), s.1(y_1))), s.1(x1)), f.0-0(x2, x3)) → F.0-1(f.1-1(s.1(y_0), s.1(y_1)), x1)
F.0-0(f.1-1(s.1(s.1(y_0)), s.1(s.1(y_1))), f.0-0(x2, x3)) → F.0-0(f.1-1(s.1(y_0), s.1(y_1)), f.0-0(x2, x3))
F.0-0(f.1-1(s.1(s.1(y_0)), s.1(0.)), f.0-0(x2, x3)) → F.0-0(f.1-1(s.1(y_0), 0.), f.0-0(x2, x3))
F.0-0(f.0-0(s.0(f.0-1(s.0(y_0), 0.)), s.0(f.0-1(s.0(s.0(y_1)), s.1(s.1(y_2))))), f.0-1(x2, x3)) → F.0-0(f.0-1(s.0(y_0), 0.), f.0-1(s.0(s.0(y_1)), s.1(s.1(y_2))))
F.0-0(f.0-1(s.0(f.1-1(s.1(s.1(y_0)), s.1(0.))), s.1(x1)), f.0-0(x2, x3)) → F.0-1(f.1-1(s.1(s.1(y_0)), s.1(0.)), x1)
F.0-0(f.0-0(s.0(f.0-1(s.0(y_0), s.1(y_1))), s.0(x1)), f.0-1(x2, x3)) → F.0-0(f.0-1(s.0(y_0), s.1(y_1)), x1)
F.0-0(f.0-1(s.0(f.1-0(s.1(s.1(y_0)), s.0(s.0(y_1)))), s.1(x1)), f.1-1(x2, x3)) → F.0-1(f.1-0(s.1(s.1(y_0)), s.0(s.0(y_1))), x1)
F.0-0(f.0-1(s.0(f.0-1(s.0(y_0), s.1(y_1))), s.1(x1)), f.1-0(x2, x3)) → F.0-1(f.0-1(s.0(y_0), s.1(y_1)), x1)
F.0-0(f.0-1(s.0(f.1-0(s.1(y_0), s.0(y_1))), s.1(x1)), f.1-1(x2, x3)) → F.0-1(f.1-0(s.1(y_0), s.0(y_1)), x1)
F.0-0(f.0-0(s.0(f.0-1(s.0(y_0), 0.)), s.0(f.1-1(s.1(s.1(y_1)), s.1(s.1(y_2))))), f.1-0(x2, x3)) → F.0-0(f.0-1(s.0(y_0), 0.), f.1-1(s.1(s.1(y_1)), s.1(s.1(y_2))))
F.0-0(f.0-0(s.0(f.1-1(s.1(y_0), s.1(y_1))), s.0(x1)), f.0-0(x2, x3)) → F.0-0(f.1-1(s.1(y_0), s.1(y_1)), x1)
F.0-0(f.0-0(s.0(f.0-1(s.0(s.0(y_0)), s.1(s.1(y_1)))), s.0(x1)), f.1-1(x2, x3)) → F.0-0(f.0-1(s.0(s.0(y_0)), s.1(s.1(y_1))), x1)
F.0-0(f.1-1(s.1(x0), 0.), f.0-1(s.0(s.0(y_0)), s.1(s.1(y_1)))) → F.0-0(f.0-1(s.0(s.0(y_0)), s.1(s.1(y_1))), f.0-1(s.0(s.0(y_0)), s.1(s.1(s.1(y_1)))))
F.0-0(f.0-0(s.0(f.1-1(s.1(y_0), 0.)), s.0(f.1-0(s.1(y_1), s.0(y_2)))), f.1-0(x2, x3)) → F.0-0(f.1-1(s.1(y_0), 0.), f.1-0(s.1(y_1), s.0(y_2)))
F.0-0(f.0-1(s.0(f.0-1(s.0(y_0), s.1(y_1))), s.1(x1)), f.0-1(x2, x3)) → F.0-1(f.0-1(s.0(y_0), s.1(y_1)), x1)
F.0-0(f.0-1(s.0(f.0-0(s.0(s.0(y_0)), s.0(s.0(y_1)))), s.1(x1)), f.0-0(x2, x3)) → F.0-1(f.0-0(s.0(s.0(y_0)), s.0(s.0(y_1))), x1)
F.0-0(f.0-0(s.0(f.1-1(s.1(s.1(y_0)), s.1(s.1(y_1)))), s.0(x1)), f.1-1(x2, x3)) → F.0-0(f.1-1(s.1(s.1(y_0)), s.1(s.1(y_1))), x1)
F.0-0(f.0-0(s.0(f.1-1(s.1(s.1(y_0)), s.1(0.))), s.0(x1)), f.0-0(x2, x3)) → F.0-0(f.1-1(s.1(s.1(y_0)), s.1(0.)), x1)
F.0-0(f.0-0(s.0(f.1-1(s.1(y_0), 0.)), s.0(f.1-0(s.1(s.1(y_1)), s.0(s.0(y_2))))), f.1-0(x2, x3)) → F.0-0(f.1-1(s.1(y_0), 0.), f.1-0(s.1(s.1(y_1)), s.0(s.0(y_2))))
F.0-0(f.0-0(s.0(f.0-0(s.0(s.0(y_0)), s.0(s.0(y_1)))), s.0(x1)), f.1-1(x2, x3)) → F.0-0(f.0-0(s.0(s.0(y_0)), s.0(s.0(y_1))), x1)
F.0-0(f.0-0(s.0(f.1-1(s.1(s.1(y_0)), s.1(0.))), s.0(x1)), f.0-1(x2, x3)) → F.0-0(f.1-1(s.1(s.1(y_0)), s.1(0.)), x1)
F.0-0(f.0-0(s.0(f.1-1(s.1(y_0), 0.)), s.0(f.0-1(s.0(y_1), s.1(y_2)))), f.0-1(x2, x3)) → F.0-0(f.1-1(s.1(y_0), 0.), f.0-1(s.0(y_1), s.1(y_2)))
F.0-0(f.0-0(s.0(f.0-1(s.0(y_0), 0.)), s.0(f.1-1(s.1(y_1), s.1(y_2)))), f.0-1(x2, x3)) → F.0-0(f.0-1(s.0(y_0), 0.), f.1-1(s.1(y_1), s.1(y_2)))
F.0-0(f.0-1(s.0(s.0(y_0)), s.1(s.1(y_1))), f.0-0(x2, x3)) → F.0-0(f.0-1(s.0(y_0), s.1(y_1)), f.0-0(x2, x3))
F.0-0(f.0-0(s.0(f.0-1(s.0(s.0(y_0)), s.1(s.1(y_1)))), s.0(x1)), f.0-1(x2, x3)) → F.0-0(f.0-1(s.0(s.0(y_0)), s.1(s.1(y_1))), x1)
F.0-0(f.0-1(s.0(f.1-1(s.1(s.1(y_0)), s.1(s.1(y_1)))), s.1(x1)), f.0-1(x2, x3)) → F.0-1(f.1-1(s.1(s.1(y_0)), s.1(s.1(y_1))), x1)
F.0-0(f.0-0(s.0(f.1-1(s.1(y_0), 0.)), s.0(f.0-1(s.0(s.0(y_1)), s.1(0.)))), f.1-1(x2, x3)) → F.0-0(f.1-1(s.1(y_0), 0.), f.0-1(s.0(s.0(y_1)), s.1(0.)))
F.0-0(f.0-0(s.0(f.1-1(s.1(y_0), 0.)), s.0(f.0-0(s.0(s.0(y_1)), s.0(s.0(y_2))))), f.1-0(x2, x3)) → F.0-0(f.1-1(s.1(y_0), 0.), f.0-0(s.0(s.0(y_1)), s.0(s.0(y_2))))
F.0-0(f.0-0(s.0(f.1-1(s.1(y_0), 0.)), s.0(f.0-0(s.0(y_1), s.0(y_2)))), f.1-0(x2, x3)) → F.0-0(f.1-1(s.1(y_0), 0.), f.0-0(s.0(y_1), s.0(y_2)))
F.0-0(f.0-0(s.0(f.0-1(s.0(y_0), 0.)), s.0(f.1-0(s.1(y_1), s.0(y_2)))), f.1-0(x2, x3)) → F.0-0(f.0-1(s.0(y_0), 0.), f.1-0(s.1(y_1), s.0(y_2)))
F.0-0(f.0-0(s.0(f.1-1(s.1(y_0), 0.)), s.0(f.0-1(s.0(s.0(y_1)), s.1(s.1(y_2))))), f.1-0(x2, x3)) → F.0-0(f.1-1(s.1(y_0), 0.), f.0-1(s.0(s.0(y_1)), s.1(s.1(y_2))))
F.0-0(f.0-0(s.0(f.0-1(s.0(s.0(y_0)), s.1(s.1(y_1)))), s.0(x1)), f.0-0(x2, x3)) → F.0-0(f.0-1(s.0(s.0(y_0)), s.1(s.1(y_1))), x1)
F.0-0(f.0-0(s.0(f.1-1(s.1(s.1(y_0)), s.1(s.1(y_1)))), s.0(x1)), f.0-0(x2, x3)) → F.0-0(f.1-1(s.1(s.1(y_0)), s.1(s.1(y_1))), x1)
F.0-0(f.0-1(s.0(x0), 0.), f.1-0(s.1(y_0), s.0(y_1))) → F.0-0(f.1-0(s.1(y_0), s.0(y_1)), f.1-0(s.1(y_0), s.0(s.0(y_1))))
F.0-0(f.0-1(s.0(x0), 0.), f.1-1(s.1(y_0), 0.)) → F.0-0(f.1-1(s.1(y_0), 0.), f.1-1(s.1(y_0), s.1(0.)))
F.0-0(f.0-1(s.0(f.1-0(s.1(s.1(y_0)), s.0(s.0(y_1)))), s.1(x1)), f.0-1(x2, x3)) → F.0-1(f.1-0(s.1(s.1(y_0)), s.0(s.0(y_1))), x1)
F.0-0(f.0-1(s.0(f.1-1(s.1(s.1(y_0)), s.1(0.))), s.1(x1)), f.1-1(x2, x3)) → F.0-1(f.1-1(s.1(s.1(y_0)), s.1(0.)), x1)
F.0-0(f.0-0(s.0(f.0-0(s.0(y_0), s.0(y_1))), s.0(x1)), f.1-1(x2, x3)) → F.0-0(f.0-0(s.0(y_0), s.0(y_1)), x1)
F.0-0(f.0-1(s.0(f.0-1(s.0(s.0(y_0)), s.1(0.))), s.1(x1)), f.1-1(x2, x3)) → F.0-1(f.0-1(s.0(s.0(y_0)), s.1(0.)), x1)
F.0-0(f.1-1(s.1(s.1(y_0)), s.1(0.)), f.1-0(x2, x3)) → F.0-0(f.1-1(s.1(y_0), 0.), f.1-0(x2, x3))
F.0-0(f.0-1(s.0(x0), 0.), f.0-1(s.0(y_0), s.1(y_1))) → F.0-0(f.0-1(s.0(y_0), s.1(y_1)), f.0-1(s.0(y_0), s.1(s.1(y_1))))
F.0-0(f.1-1(s.1(s.1(y_0)), s.1(s.1(y_1))), f.0-1(x2, x3)) → F.0-0(f.1-1(s.1(y_0), s.1(y_1)), f.0-1(x2, x3))
F.0-0(f.0-0(s.0(f.0-1(s.0(y_0), 0.)), s.0(f.1-1(s.1(s.1(y_1)), s.1(s.1(y_2))))), f.0-1(x2, x3)) → F.0-0(f.0-1(s.0(y_0), 0.), f.1-1(s.1(s.1(y_1)), s.1(s.1(y_2))))
F.0-0(f.1-1(s.1(x0), 0.), f.0-1(s.0(s.0(y_0)), s.1(0.))) → F.0-0(f.0-1(s.0(s.0(y_0)), s.1(0.)), f.0-1(s.0(s.0(y_0)), s.1(s.1(0.))))
F.0-0(f.0-1(s.0(f.0-1(s.0(y_0), s.1(y_1))), s.1(x1)), f.0-0(x2, x3)) → F.0-1(f.0-1(s.0(y_0), s.1(y_1)), x1)
F.0-0(f.0-1(s.0(f.0-0(s.0(s.0(y_0)), s.0(s.0(y_1)))), s.1(x1)), f.1-0(x2, x3)) → F.0-1(f.0-0(s.0(s.0(y_0)), s.0(s.0(y_1))), x1)
F.0-0(f.0-1(s.0(x0), 0.), f.1-1(s.1(s.1(y_0)), s.1(0.))) → F.0-0(f.1-1(s.1(s.1(y_0)), s.1(0.)), f.1-1(s.1(s.1(y_0)), s.1(s.1(0.))))
F.0-0(f.0-0(s.0(f.1-1(s.1(y_0), 0.)), s.0(f.0-1(s.0(s.0(y_1)), s.1(s.1(y_2))))), f.0-0(x2, x3)) → F.0-0(f.1-1(s.1(y_0), 0.), f.0-1(s.0(s.0(y_1)), s.1(s.1(y_2))))
F.0-0(f.0-0(s.0(f.0-1(s.0(y_0), s.1(y_1))), s.0(x1)), f.1-1(x2, x3)) → F.0-0(f.0-1(s.0(y_0), s.1(y_1)), x1)
F.0-0(f.0-0(s.0(f.0-1(s.0(y_0), 0.)), s.0(f.0-1(s.0(y_1), s.1(y_2)))), f.0-1(x2, x3)) → F.0-0(f.0-1(s.0(y_0), 0.), f.0-1(s.0(y_1), s.1(y_2)))
F.0-0(f.0-0(s.0(f.1-1(s.1(y_0), 0.)), s.0(f.1-1(s.1(s.1(y_1)), s.1(s.1(y_2))))), f.0-1(x2, x3)) → F.0-0(f.1-1(s.1(y_0), 0.), f.1-1(s.1(s.1(y_1)), s.1(s.1(y_2))))
F.0-0(f.0-1(s.0(f.1-0(s.1(y_0), s.0(y_1))), s.1(x1)), f.0-1(x2, x3)) → F.0-1(f.1-0(s.1(y_0), s.0(y_1)), x1)
F.0-0(f.0-0(s.0(f.0-1(s.0(y_0), 0.)), s.0(f.0-0(s.0(y_1), s.0(y_2)))), f.0-1(x2, x3)) → F.0-0(f.0-1(s.0(y_0), 0.), f.0-0(s.0(y_1), s.0(y_2)))
F.0-0(f.0-0(s.0(f.0-1(s.0(y_0), 0.)), s.0(f.0-1(s.0(y_1), 0.))), f.1-1(x2, x3)) → F.0-0(f.0-1(s.0(y_0), 0.), f.0-1(s.0(y_1), 0.))
F.0-0(f.0-1(s.0(f.1-0(s.1(y_0), s.0(y_1))), s.1(x1)), f.0-0(x2, x3)) → F.0-1(f.1-0(s.1(y_0), s.0(y_1)), x1)
F.0-0(f.0-0(s.0(f.1-1(s.1(y_0), 0.)), s.0(f.1-1(s.1(y_1), 0.))), f.1-1(x2, x3)) → F.0-0(f.1-1(s.1(y_0), 0.), f.1-1(s.1(y_1), 0.))
F.0-0(f.0-0(s.0(f.1-1(s.1(y_0), 0.)), s.0(f.1-1(s.1(y_1), 0.))), f.0-0(x2, x3)) → F.0-0(f.1-1(s.1(y_0), 0.), f.1-1(s.1(y_1), 0.))
F.0-0(f.0-1(s.0(s.0(y_0)), s.1(0.)), f.1-0(x2, x3)) → F.0-0(f.0-1(s.0(y_0), 0.), f.1-0(x2, x3))
F.0-0(f.0-1(s.0(f.1-0(s.1(s.1(y_0)), s.0(s.0(y_1)))), s.1(x1)), f.1-0(x2, x3)) → F.0-1(f.1-0(s.1(s.1(y_0)), s.0(s.0(y_1))), x1)
F.0-0(f.0-1(s.0(s.0(y_0)), s.1(s.1(y_1))), f.1-1(x2, x3)) → F.0-0(f.0-1(s.0(y_0), s.1(y_1)), f.1-1(x2, x3))
F.0-0(f.0-1(s.0(x0), 0.), f.0-0(s.0(s.0(y_0)), s.0(s.0(y_1)))) → F.0-0(f.0-0(s.0(s.0(y_0)), s.0(s.0(y_1))), f.0-0(s.0(s.0(y_0)), s.0(s.0(s.0(y_1)))))
F.0-0(f.0-0(s.0(f.0-1(s.0(y_0), 0.)), s.0(f.1-1(s.1(s.1(y_1)), s.1(0.)))), f.0-0(x2, x3)) → F.0-0(f.0-1(s.0(y_0), 0.), f.1-1(s.1(s.1(y_1)), s.1(0.)))
F.0-0(f.0-0(s.0(f.1-1(s.1(y_0), 0.)), s.0(f.1-1(s.1(y_1), 0.))), f.1-0(x2, x3)) → F.0-0(f.1-1(s.1(y_0), 0.), f.1-1(s.1(y_1), 0.))
F.0-0(f.0-1(s.0(f.1-1(s.1(s.1(y_0)), s.1(s.1(y_1)))), s.1(x1)), f.1-0(x2, x3)) → F.0-1(f.1-1(s.1(s.1(y_0)), s.1(s.1(y_1))), x1)
F.0-0(f.0-0(s.0(f.1-1(s.1(y_0), 0.)), s.0(f.1-1(s.1(y_1), s.1(y_2)))), f.0-0(x2, x3)) → F.0-0(f.1-1(s.1(y_0), 0.), f.1-1(s.1(y_1), s.1(y_2)))
F.0-0(f.0-0(s.0(f.1-1(s.1(y_0), 0.)), s.0(f.0-1(s.0(s.0(y_1)), s.1(0.)))), f.0-0(x2, x3)) → F.0-0(f.1-1(s.1(y_0), 0.), f.0-1(s.0(s.0(y_1)), s.1(0.)))
F.0-0(f.0-0(s.0(f.0-0(s.0(y_0), s.0(y_1))), s.0(x1)), f.1-0(x2, x3)) → F.0-0(f.0-0(s.0(y_0), s.0(y_1)), x1)
F.0-0(f.0-1(s.0(f.0-0(s.0(y_0), s.0(y_1))), s.1(x1)), f.0-1(x2, x3)) → F.0-1(f.0-0(s.0(y_0), s.0(y_1)), x1)
F.0-0(f.0-1(s.0(f.0-1(s.0(s.0(y_0)), s.1(s.1(y_1)))), s.1(x1)), f.0-1(x2, x3)) → F.0-1(f.0-1(s.0(s.0(y_0)), s.1(s.1(y_1))), x1)
F.0-0(f.0-0(s.0(f.0-1(s.0(y_0), 0.)), s.0(f.1-0(s.1(s.1(y_1)), s.0(s.0(y_2))))), f.0-1(x2, x3)) → F.0-0(f.0-1(s.0(y_0), 0.), f.1-0(s.1(s.1(y_1)), s.0(s.0(y_2))))
F.0-0(f.0-1(s.0(f.0-1(s.0(s.0(y_0)), s.1(0.))), s.1(x1)), f.0-0(x2, x3)) → F.0-1(f.0-1(s.0(s.0(y_0)), s.1(0.)), x1)
F.0-0(f.0-0(s.0(f.1-1(s.1(y_0), 0.)), s.0(f.1-1(s.1(s.1(y_1)), s.1(0.)))), f.1-1(x2, x3)) → F.0-0(f.1-1(s.1(y_0), 0.), f.1-1(s.1(s.1(y_1)), s.1(0.)))
F.0-0(f.0-0(s.0(f.0-1(s.0(y_0), 0.)), s.0(f.0-0(s.0(s.0(y_1)), s.0(s.0(y_2))))), f.1-1(x2, x3)) → F.0-0(f.0-1(s.0(y_0), 0.), f.0-0(s.0(s.0(y_1)), s.0(s.0(y_2))))
F.0-0(f.0-1(s.0(x0), 0.), f.0-1(s.0(y_0), 0.)) → F.0-0(f.0-1(s.0(y_0), 0.), f.0-1(s.0(y_0), s.1(0.)))
F.0-0(f.0-0(s.0(f.1-1(s.1(y_0), s.1(y_1))), s.0(x1)), f.0-1(x2, x3)) → F.0-0(f.1-1(s.1(y_0), s.1(y_1)), x1)
F.0-0(f.0-0(s.0(f.1-1(s.1(y_0), 0.)), s.0(f.1-1(s.1(y_1), s.1(y_2)))), f.0-1(x2, x3)) → F.0-0(f.1-1(s.1(y_0), 0.), f.1-1(s.1(y_1), s.1(y_2)))
F.0-0(f.0-0(s.0(f.1-1(s.1(s.1(y_0)), s.1(s.1(y_1)))), s.0(x1)), f.0-1(x2, x3)) → F.0-0(f.1-1(s.1(s.1(y_0)), s.1(s.1(y_1))), x1)
F.0-0(f.0-0(s.0(f.1-1(s.1(y_0), 0.)), s.0(f.0-0(s.0(s.0(y_1)), s.0(s.0(y_2))))), f.0-1(x2, x3)) → F.0-0(f.1-1(s.1(y_0), 0.), f.0-0(s.0(s.0(y_1)), s.0(s.0(y_2))))
F.0-0(f.0-1(s.0(f.1-1(s.1(y_0), s.1(y_1))), s.1(x1)), f.1-1(x2, x3)) → F.0-1(f.1-1(s.1(y_0), s.1(y_1)), x1)
F.0-0(f.0-0(s.0(f.0-0(s.0(s.0(y_0)), s.0(s.0(y_1)))), s.0(x1)), f.0-0(x2, x3)) → F.0-0(f.0-0(s.0(s.0(y_0)), s.0(s.0(y_1))), x1)
F.0-0(f.0-0(s.0(f.0-1(s.0(y_0), 0.)), s.0(f.1-1(s.1(y_1), 0.))), f.1-1(x2, x3)) → F.0-0(f.0-1(s.0(y_0), 0.), f.1-1(s.1(y_1), 0.))
F.0-0(f.0-0(s.0(f.1-1(s.1(y_0), 0.)), s.0(f.0-1(s.0(y_1), 0.))), f.1-1(x2, x3)) → F.0-0(f.1-1(s.1(y_0), 0.), f.0-1(s.0(y_1), 0.))
F.0-0(f.0-1(s.0(f.0-0(s.0(y_0), s.0(y_1))), s.1(x1)), f.1-1(x2, x3)) → F.0-1(f.0-0(s.0(y_0), s.0(y_1)), x1)
F.0-0(f.0-0(s.0(f.1-1(s.1(y_0), 0.)), s.0(f.1-1(s.1(y_1), s.1(y_2)))), f.1-0(x2, x3)) → F.0-0(f.1-1(s.1(y_0), 0.), f.1-1(s.1(y_1), s.1(y_2)))
F.0-0(f.0-0(s.0(f.1-1(s.1(y_0), 0.)), s.0(f.0-1(s.0(s.0(y_1)), s.1(0.)))), f.0-1(x2, x3)) → F.0-0(f.1-1(s.1(y_0), 0.), f.0-1(s.0(s.0(y_1)), s.1(0.)))
F.0-0(f.0-0(s.0(f.1-1(s.1(y_0), 0.)), s.0(f.0-1(s.0(y_1), s.1(y_2)))), f.1-1(x2, x3)) → F.0-0(f.1-1(s.1(y_0), 0.), f.0-1(s.0(y_1), s.1(y_2)))
F.0-0(f.0-0(s.0(f.0-1(s.0(y_0), 0.)), s.0(f.1-1(s.1(y_1), s.1(y_2)))), f.1-1(x2, x3)) → F.0-0(f.0-1(s.0(y_0), 0.), f.1-1(s.1(y_1), s.1(y_2)))
F.0-0(f.0-0(s.0(f.0-1(s.0(y_0), 0.)), s.0(f.0-0(s.0(s.0(y_1)), s.0(s.0(y_2))))), f.0-0(x2, x3)) → F.0-0(f.0-1(s.0(y_0), 0.), f.0-0(s.0(s.0(y_1)), s.0(s.0(y_2))))
F.0-0(f.0-1(s.0(x0), 0.), f.0-1(s.0(s.0(y_0)), s.1(0.))) → F.0-0(f.0-1(s.0(s.0(y_0)), s.1(0.)), f.0-1(s.0(s.0(y_0)), s.1(s.1(0.))))
F.0-0(f.0-1(s.0(f.0-1(s.0(s.0(y_0)), s.1(0.))), s.1(x1)), f.1-0(x2, x3)) → F.0-1(f.0-1(s.0(s.0(y_0)), s.1(0.)), x1)
F.0-0(f.0-0(s.0(f.0-1(s.0(y_0), 0.)), s.0(f.0-1(s.0(s.0(y_1)), s.1(s.1(y_2))))), f.0-0(x2, x3)) → F.0-0(f.0-1(s.0(y_0), 0.), f.0-1(s.0(s.0(y_1)), s.1(s.1(y_2))))
F.0-0(f.0-1(s.0(f.0-1(s.0(s.0(y_0)), s.1(s.1(y_1)))), s.1(x1)), f.1-0(x2, x3)) → F.0-1(f.0-1(s.0(s.0(y_0)), s.1(s.1(y_1))), x1)
F.0-0(f.0-1(s.0(f.0-1(s.0(s.0(y_0)), s.1(s.1(y_1)))), s.1(x1)), f.1-1(x2, x3)) → F.0-1(f.0-1(s.0(s.0(y_0)), s.1(s.1(y_1))), x1)
F.0-0(f.0-0(s.0(f.1-1(s.1(y_0), 0.)), s.0(f.1-1(s.1(s.1(y_1)), s.1(0.)))), f.1-0(x2, x3)) → F.0-0(f.1-1(s.1(y_0), 0.), f.1-1(s.1(s.1(y_1)), s.1(0.)))
F.0-0(f.0-1(s.0(f.0-1(s.0(s.0(y_0)), s.1(s.1(y_1)))), s.1(x1)), f.0-0(x2, x3)) → F.0-1(f.0-1(s.0(s.0(y_0)), s.1(s.1(y_1))), x1)
F.0-0(f.0-0(s.0(f.0-0(s.0(y_0), s.0(y_1))), s.0(x1)), f.0-0(x2, x3)) → F.0-0(f.0-0(s.0(y_0), s.0(y_1)), x1)
F.0-0(f.0-1(s.0(f.0-1(s.0(y_0), s.1(y_1))), s.1(x1)), f.1-1(x2, x3)) → F.0-1(f.0-1(s.0(y_0), s.1(y_1)), x1)
F.0-0(f.1-1(s.1(x0), 0.), f.1-1(s.1(s.1(y_0)), s.1(s.1(y_1)))) → F.0-0(f.1-1(s.1(s.1(y_0)), s.1(s.1(y_1))), f.1-1(s.1(s.1(y_0)), s.1(s.1(s.1(y_1)))))
F.0-0(f.0-0(s.0(f.1-1(s.1(y_0), 0.)), s.0(f.1-0(s.1(s.1(y_1)), s.0(s.0(y_2))))), f.0-0(x2, x3)) → F.0-0(f.1-1(s.1(y_0), 0.), f.1-0(s.1(s.1(y_1)), s.0(s.0(y_2))))
F.0-0(f.1-1(s.1(x0), 0.), f.0-1(s.0(y_0), s.1(y_1))) → F.0-0(f.0-1(s.0(y_0), s.1(y_1)), f.0-1(s.0(y_0), s.1(s.1(y_1))))
F.0-0(f.0-0(s.0(f.1-1(s.1(y_0), 0.)), s.0(f.1-0(s.1(y_1), s.0(y_2)))), f.0-1(x2, x3)) → F.0-0(f.1-1(s.1(y_0), 0.), f.1-0(s.1(y_1), s.0(y_2)))
F.0-0(f.1-1(s.1(x0), 0.), f.1-0(s.1(y_0), s.0(y_1))) → F.0-0(f.1-0(s.1(y_0), s.0(y_1)), f.1-0(s.1(y_0), s.0(s.0(y_1))))
F.0-0(f.1-1(s.1(s.1(y_0)), s.1(0.)), f.0-1(x2, x3)) → F.0-0(f.1-1(s.1(y_0), 0.), f.0-1(x2, x3))
F.0-0(f.1-1(s.1(x0), 0.), f.1-1(s.1(y_0), 0.)) → F.0-0(f.1-1(s.1(y_0), 0.), f.1-1(s.1(y_0), s.1(0.)))
F.0-0(f.0-0(s.0(f.1-1(s.1(y_0), s.1(y_1))), s.0(x1)), f.1-0(x2, x3)) → F.0-0(f.1-1(s.1(y_0), s.1(y_1)), x1)
F.0-0(f.0-0(s.0(f.1-0(s.1(y_0), s.0(y_1))), s.0(x1)), f.1-0(x2, x3)) → F.0-0(f.1-0(s.1(y_0), s.0(y_1)), x1)
F.0-0(f.0-0(s.0(f.0-1(s.0(y_0), 0.)), s.0(f.1-1(s.1(s.1(y_1)), s.1(s.1(y_2))))), f.1-1(x2, x3)) → F.0-0(f.0-1(s.0(y_0), 0.), f.1-1(s.1(s.1(y_1)), s.1(s.1(y_2))))
F.0-0(f.0-1(s.0(f.1-1(s.1(s.1(y_0)), s.1(s.1(y_1)))), s.1(x1)), f.0-0(x2, x3)) → F.0-1(f.1-1(s.1(s.1(y_0)), s.1(s.1(y_1))), x1)
F.0-0(f.0-0(s.0(s.0(y_0)), s.0(s.0(y_1))), f.0-1(x2, x3)) → F.0-0(f.0-0(s.0(y_0), s.0(y_1)), f.0-1(x2, x3))
F.0-0(f.0-1(s.0(x0), 0.), f.1-0(s.1(s.1(y_0)), s.0(s.0(y_1)))) → F.0-0(f.1-0(s.1(s.1(y_0)), s.0(s.0(y_1))), f.1-0(s.1(s.1(y_0)), s.0(s.0(s.0(y_1)))))
F.0-0(f.1-1(s.1(x0), 0.), f.1-1(s.1(s.1(y_0)), s.1(0.))) → F.0-0(f.1-1(s.1(s.1(y_0)), s.1(0.)), f.1-1(s.1(s.1(y_0)), s.1(s.1(0.))))
F.0-0(f.0-1(s.0(f.0-0(s.0(s.0(y_0)), s.0(s.0(y_1)))), s.1(x1)), f.1-1(x2, x3)) → F.0-1(f.0-0(s.0(s.0(y_0)), s.0(s.0(y_1))), x1)
F.0-0(f.1-0(s.1(s.1(y_0)), s.0(s.0(y_1))), f.0-0(x2, x3)) → F.0-0(f.1-0(s.1(y_0), s.0(y_1)), f.0-0(x2, x3))
F.0-0(f.1-0(s.1(s.1(y_0)), s.0(s.0(y_1))), f.1-0(x2, x3)) → F.0-0(f.1-0(s.1(y_0), s.0(y_1)), f.1-0(x2, x3))
F.0-0(f.0-0(s.0(s.0(y_0)), s.0(s.0(y_1))), f.0-0(x2, x3)) → F.0-0(f.0-0(s.0(y_0), s.0(y_1)), f.0-0(x2, x3))
F.0-0(f.0-0(s.0(f.0-1(s.0(s.0(y_0)), s.1(0.))), s.0(x1)), f.1-1(x2, x3)) → F.0-0(f.0-1(s.0(s.0(y_0)), s.1(0.)), x1)
F.0-0(f.1-1(s.1(s.1(y_0)), s.1(s.1(y_1))), f.1-1(x2, x3)) → F.0-0(f.1-1(s.1(y_0), s.1(y_1)), f.1-1(x2, x3))
F.0-0(f.0-0(s.0(s.0(y_0)), s.0(s.0(y_1))), f.1-1(x2, x3)) → F.0-0(f.0-0(s.0(y_0), s.0(y_1)), f.1-1(x2, x3))
F.0-0(f.0-1(s.0(x0), 0.), f.0-0(s.0(y_0), s.0(y_1))) → F.0-0(f.0-0(s.0(y_0), s.0(y_1)), f.0-0(s.0(y_0), s.0(s.0(y_1))))
F.0-0(f.1-0(s.1(s.1(y_0)), s.0(s.0(y_1))), f.1-1(x2, x3)) → F.0-0(f.1-0(s.1(y_0), s.0(y_1)), f.1-1(x2, x3))
F.0-0(f.0-1(s.0(f.1-1(s.1(y_0), s.1(y_1))), s.1(x1)), f.1-0(x2, x3)) → F.0-1(f.1-1(s.1(y_0), s.1(y_1)), x1)
F.0-0(f.0-0(s.0(f.0-1(s.0(y_0), 0.)), s.0(f.1-1(s.1(y_1), 0.))), f.0-1(x2, x3)) → F.0-0(f.0-1(s.0(y_0), 0.), f.1-1(s.1(y_1), 0.))
F.0-0(f.0-0(s.0(f.1-1(s.1(y_0), 0.)), s.0(f.0-1(s.0(y_1), 0.))), f.0-1(x2, x3)) → F.0-0(f.1-1(s.1(y_0), 0.), f.0-1(s.0(y_1), 0.))
F.0-0(f.0-0(s.0(f.1-1(s.1(s.1(y_0)), s.1(s.1(y_1)))), s.0(x1)), f.1-0(x2, x3)) → F.0-0(f.1-1(s.1(s.1(y_0)), s.1(s.1(y_1))), x1)
F.0-0(f.0-0(s.0(f.1-1(s.1(y_0), 0.)), s.0(f.0-1(s.0(s.0(y_1)), s.1(0.)))), f.1-0(x2, x3)) → F.0-0(f.1-1(s.1(y_0), 0.), f.0-1(s.0(s.0(y_1)), s.1(0.)))
F.0-0(f.0-0(s.0(f.1-0(s.1(s.1(y_0)), s.0(s.0(y_1)))), s.0(x1)), f.0-0(x2, x3)) → F.0-0(f.1-0(s.1(s.1(y_0)), s.0(s.0(y_1))), x1)
F.0-0(f.0-0(s.0(f.1-1(s.1(y_0), 0.)), s.0(f.0-0(s.0(y_1), s.0(y_2)))), f.1-1(x2, x3)) → F.0-0(f.1-1(s.1(y_0), 0.), f.0-0(s.0(y_1), s.0(y_2)))
F.0-0(f.0-0(s.0(f.0-1(s.0(y_0), 0.)), s.0(f.1-0(s.1(y_1), s.0(y_2)))), f.1-1(x2, x3)) → F.0-0(f.0-1(s.0(y_0), 0.), f.1-0(s.1(y_1), s.0(y_2)))
F.0-0(f.0-0(s.0(f.0-0(s.0(y_0), s.0(y_1))), s.0(x1)), f.0-1(x2, x3)) → F.0-0(f.0-0(s.0(y_0), s.0(y_1)), x1)
F.0-0(f.0-0(s.0(f.0-1(s.0(s.0(y_0)), s.1(0.))), s.0(x1)), f.0-1(x2, x3)) → F.0-0(f.0-1(s.0(s.0(y_0)), s.1(0.)), x1)
F.0-0(f.0-0(s.0(s.0(y_0)), s.0(s.0(y_1))), f.1-0(x2, x3)) → F.0-0(f.0-0(s.0(y_0), s.0(y_1)), f.1-0(x2, x3))
F.0-0(f.0-1(s.0(s.0(y_0)), s.1(0.)), f.0-1(x2, x3)) → F.0-0(f.0-1(s.0(y_0), 0.), f.0-1(x2, x3))
F.0-0(f.0-1(s.0(s.0(y_0)), s.1(s.1(y_1))), f.0-1(x2, x3)) → F.0-0(f.0-1(s.0(y_0), s.1(y_1)), f.0-1(x2, x3))
F.0-0(f.0-0(s.0(f.0-1(s.0(y_0), 0.)), s.0(f.0-1(s.0(s.0(y_1)), s.1(0.)))), f.0-0(x2, x3)) → F.0-0(f.0-1(s.0(y_0), 0.), f.0-1(s.0(s.0(y_1)), s.1(0.)))
F.0-0(f.1-1(s.1(x0), 0.), f.0-0(s.0(y_0), s.0(y_1))) → F.0-0(f.0-0(s.0(y_0), s.0(y_1)), f.0-0(s.0(y_0), s.0(s.0(y_1))))
F.0-0(f.0-0(s.0(f.1-1(s.1(y_0), s.1(y_1))), s.0(x1)), f.1-1(x2, x3)) → F.0-0(f.1-1(s.1(y_0), s.1(y_1)), x1)
F.0-0(f.0-0(s.0(f.0-1(s.0(s.0(y_0)), s.1(0.))), s.0(x1)), f.0-0(x2, x3)) → F.0-0(f.0-1(s.0(s.0(y_0)), s.1(0.)), x1)
F.0-0(f.0-0(s.0(f.1-1(s.1(y_0), 0.)), s.0(f.0-0(s.0(s.0(y_1)), s.0(s.0(y_2))))), f.0-0(x2, x3)) → F.0-0(f.1-1(s.1(y_0), 0.), f.0-0(s.0(s.0(y_1)), s.0(s.0(y_2))))
F.0-0(f.0-1(s.0(f.1-1(s.1(y_0), s.1(y_1))), s.1(x1)), f.0-1(x2, x3)) → F.0-1(f.1-1(s.1(y_0), s.1(y_1)), x1)
F.0-0(f.0-0(s.0(f.0-1(s.0(y_0), 0.)), s.0(f.1-1(s.1(y_1), 0.))), f.0-0(x2, x3)) → F.0-0(f.0-1(s.0(y_0), 0.), f.1-1(s.1(y_1), 0.))
F.0-0(f.0-0(s.0(f.1-1(s.1(y_0), 0.)), s.0(f.0-1(s.0(y_1), 0.))), f.0-0(x2, x3)) → F.0-0(f.1-1(s.1(y_0), 0.), f.0-1(s.0(y_1), 0.))
F.0-0(f.0-1(s.0(f.1-1(s.1(s.1(y_0)), s.1(s.1(y_1)))), s.1(x1)), f.1-1(x2, x3)) → F.0-1(f.1-1(s.1(s.1(y_0)), s.1(s.1(y_1))), x1)
F.0-0(f.0-0(s.0(f.0-0(s.0(s.0(y_0)), s.0(s.0(y_1)))), s.0(x1)), f.1-0(x2, x3)) → F.0-0(f.0-0(s.0(s.0(y_0)), s.0(s.0(y_1))), x1)
F.0-0(f.0-1(s.0(s.0(y_0)), s.1(0.)), f.1-1(x2, x3)) → F.0-0(f.0-1(s.0(y_0), 0.), f.1-1(x2, x3))
F.0-0(f.0-1(s.0(s.0(y_0)), s.1(s.1(y_1))), f.1-0(x2, x3)) → F.0-0(f.0-1(s.0(y_0), s.1(y_1)), f.1-0(x2, x3))
F.0-0(f.1-0(s.1(s.1(y_0)), s.0(s.0(y_1))), f.0-1(x2, x3)) → F.0-0(f.1-0(s.1(y_0), s.0(y_1)), f.0-1(x2, x3))
F.0-0(f.0-0(s.0(f.1-1(s.1(y_0), 0.)), s.0(f.0-0(s.0(y_1), s.0(y_2)))), f.0-1(x2, x3)) → F.0-0(f.1-1(s.1(y_0), 0.), f.0-0(s.0(y_1), s.0(y_2)))
F.0-0(f.0-0(s.0(f.0-1(s.0(y_0), 0.)), s.0(f.1-0(s.1(y_1), s.0(y_2)))), f.0-1(x2, x3)) → F.0-0(f.0-1(s.0(y_0), 0.), f.1-0(s.1(y_1), s.0(y_2)))
F.0-0(f.0-0(s.0(f.0-1(s.0(y_0), 0.)), s.0(f.0-1(s.0(y_1), 0.))), f.1-0(x2, x3)) → F.0-0(f.0-1(s.0(y_0), 0.), f.0-1(s.0(y_1), 0.))
F.0-0(f.0-0(s.0(f.0-1(s.0(y_0), 0.)), s.0(f.0-1(s.0(s.0(y_1)), s.1(0.)))), f.1-1(x2, x3)) → F.0-0(f.0-1(s.0(y_0), 0.), f.0-1(s.0(s.0(y_1)), s.1(0.)))
F.0-0(f.0-0(s.0(f.0-1(s.0(y_0), 0.)), s.0(f.0-1(s.0(y_1), 0.))), f.0-0(x2, x3)) → F.0-0(f.0-1(s.0(y_0), 0.), f.0-1(s.0(y_1), 0.))
F.0-0(f.0-0(s.0(f.0-1(s.0(y_0), 0.)), s.0(f.1-0(s.1(s.1(y_1)), s.0(s.0(y_2))))), f.0-0(x2, x3)) → F.0-0(f.0-1(s.0(y_0), 0.), f.1-0(s.1(s.1(y_1)), s.0(s.0(y_2))))
f.0-0(f.0-0(s.0(x), s.0(y)), f.1-0(z, w)) → f.0-0(f.0-0(x, y), f.1-0(z, w))
f.0-0(f.1-1(s.1(x), s.1(y)), f.1-0(z, w)) → f.0-0(f.1-1(x, y), f.1-0(z, w))
f.0-0(f.0-1(s.0(x), s.1(y)), f.0-1(z, w)) → f.0-0(f.0-1(x, y), f.0-1(z, w))
f.0-0(f.0-0(s.0(x), s.0(y)), f.0-1(z, w)) → f.0-0(f.0-0(x, y), f.0-1(z, w))
f.0-0(f.0-1(s.0(x), 0.), f.1-1(y, z)) → f.0-0(f.1-1(y, z), f.1-1(y, s.1(z)))
f.0-0(f.1-1(s.1(x), 0.), f.0-1(y, z)) → f.0-0(f.0-1(y, z), f.0-1(y, s.1(z)))
f.0-0(f.1-1(s.1(x), s.1(y)), f.0-1(z, w)) → f.0-0(f.1-1(x, y), f.0-1(z, w))
f.0-0(f.1-1(s.1(x), s.1(y)), f.0-0(z, w)) → f.0-0(f.1-1(x, y), f.0-0(z, w))
f.0-0(f.0-0(s.0(x), s.0(y)), f.1-1(z, w)) → f.0-0(f.0-0(x, y), f.1-1(z, w))
f.0-0(f.0-1(s.0(x), 0.), f.0-0(y, z)) → f.0-0(f.0-0(y, z), f.0-0(y, s.0(z)))
f.0-0(f.1-1(s.1(x), 0.), f.0-0(y, z)) → f.0-0(f.0-0(y, z), f.0-0(y, s.0(z)))
f.0-0(f.0-1(s.0(x), 0.), f.0-1(y, z)) → f.0-0(f.0-1(y, z), f.0-1(y, s.1(z)))
f.0-0(f.1-1(s.1(x), s.1(y)), f.1-1(z, w)) → f.0-0(f.1-1(x, y), f.1-1(z, w))
f.0-0(f.0-0(s.0(x), s.0(y)), f.0-0(z, w)) → f.0-0(f.0-0(x, y), f.0-0(z, w))
f.0-0(f.1-1(s.1(x), 0.), f.1-0(y, z)) → f.0-0(f.1-0(y, z), f.1-0(y, s.0(z)))
f.0-0(f.0-1(s.0(x), s.1(y)), f.0-0(z, w)) → f.0-0(f.0-1(x, y), f.0-0(z, w))
f.0-0(f.1-0(s.1(x), s.0(y)), f.1-0(z, w)) → f.0-0(f.1-0(x, y), f.1-0(z, w))
f.0-0(f.1-0(s.1(x), s.0(y)), f.0-1(z, w)) → f.0-0(f.1-0(x, y), f.0-1(z, w))
f.0-0(f.0-1(s.0(x), s.1(y)), f.1-0(z, w)) → f.0-0(f.0-1(x, y), f.1-0(z, w))
f.0-0(f.0-1(s.0(x), s.1(y)), f.1-1(z, w)) → f.0-0(f.0-1(x, y), f.1-1(z, w))
f.0-0(f.1-1(s.1(x), 0.), f.1-1(y, z)) → f.0-0(f.1-1(y, z), f.1-1(y, s.1(z)))
f.0-0(f.1-0(s.1(x), s.0(y)), f.0-0(z, w)) → f.0-0(f.1-0(x, y), f.0-0(z, w))
f.0-0(f.0-1(s.0(x), 0.), f.1-0(y, z)) → f.0-0(f.1-0(y, z), f.1-0(y, s.0(z)))
f.0-0(f.1-0(s.1(x), s.0(y)), f.1-1(z, w)) → f.0-0(f.1-0(x, y), f.1-1(z, w))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ SemLabProof
↳ QDP
↳ DependencyGraphProof
↳ SemLabProof2
F.0-0(f.0-0(s.0(f.0-1(s.0(y_0), 0.)), s.0(f.0-1(s.0(s.0(y_1)), s.1(0.)))), f.1-0(x2, x3)) → F.0-0(f.0-1(s.0(y_0), 0.), f.0-1(s.0(s.0(y_1)), s.1(0.)))
F.0-0(f.0-0(s.0(f.1-1(s.1(s.1(y_0)), s.1(0.))), s.0(x1)), f.1-1(x2, x3)) → F.0-0(f.1-1(s.1(s.1(y_0)), s.1(0.)), x1)
F.0-0(f.0-0(s.0(f.0-1(s.0(y_0), 0.)), s.0(f.0-1(s.0(y_1), 0.))), f.0-1(x2, x3)) → F.0-0(f.0-1(s.0(y_0), 0.), f.0-1(s.0(y_1), 0.))
F.0-0(f.0-0(s.0(f.0-1(s.0(y_0), 0.)), s.0(f.0-0(s.0(y_1), s.0(y_2)))), f.1-1(x2, x3)) → F.0-0(f.0-1(s.0(y_0), 0.), f.0-0(s.0(y_1), s.0(y_2)))
F.0-0(f.0-0(s.0(f.0-1(s.0(y_0), 0.)), s.0(f.0-1(s.0(s.0(y_1)), s.1(0.)))), f.0-1(x2, x3)) → F.0-0(f.0-1(s.0(y_0), 0.), f.0-1(s.0(s.0(y_1)), s.1(0.)))
F.0-0(f.0-0(s.0(f.0-1(s.0(y_0), 0.)), s.0(f.1-0(s.1(s.1(y_1)), s.0(s.0(y_2))))), f.1-0(x2, x3)) → F.0-0(f.0-1(s.0(y_0), 0.), f.1-0(s.1(s.1(y_1)), s.0(s.0(y_2))))
F.0-0(f.0-0(s.0(f.1-0(s.1(y_0), s.0(y_1))), s.0(x1)), f.0-0(x2, x3)) → F.0-0(f.1-0(s.1(y_0), s.0(y_1)), x1)
F.0-0(f.0-0(s.0(f.1-1(s.1(y_0), 0.)), s.0(f.0-1(s.0(y_1), s.1(y_2)))), f.0-0(x2, x3)) → F.0-0(f.1-1(s.1(y_0), 0.), f.0-1(s.0(y_1), s.1(y_2)))
F.0-0(f.0-0(s.0(f.0-1(s.0(y_0), 0.)), s.0(f.1-1(s.1(y_1), s.1(y_2)))), f.0-0(x2, x3)) → F.0-0(f.0-1(s.0(y_0), 0.), f.1-1(s.1(y_1), s.1(y_2)))
F.0-0(f.0-1(s.0(s.0(y_0)), s.1(0.)), f.0-0(x2, x3)) → F.0-0(f.0-1(s.0(y_0), 0.), f.0-0(x2, x3))
F.0-0(f.0-0(s.0(f.0-1(s.0(y_0), 0.)), s.0(f.0-0(s.0(y_1), s.0(y_2)))), f.1-0(x2, x3)) → F.0-0(f.0-1(s.0(y_0), 0.), f.0-0(s.0(y_1), s.0(y_2)))
F.0-0(f.0-1(s.0(f.1-0(s.1(y_0), s.0(y_1))), s.1(x1)), f.1-0(x2, x3)) → F.0-1(f.1-0(s.1(y_0), s.0(y_1)), x1)
F.0-0(f.0-0(s.0(f.0-1(s.0(y_0), 0.)), s.0(f.1-1(s.1(y_1), 0.))), f.1-0(x2, x3)) → F.0-0(f.0-1(s.0(y_0), 0.), f.1-1(s.1(y_1), 0.))
F.0-0(f.0-0(s.0(f.1-1(s.1(y_0), 0.)), s.0(f.0-1(s.0(y_1), 0.))), f.1-0(x2, x3)) → F.0-0(f.1-1(s.1(y_0), 0.), f.0-1(s.0(y_1), 0.))
F.0-0(f.0-0(s.0(f.0-1(s.0(y_0), 0.)), s.0(f.0-0(s.0(y_1), s.0(y_2)))), f.0-0(x2, x3)) → F.0-0(f.0-1(s.0(y_0), 0.), f.0-0(s.0(y_1), s.0(y_2)))
F.0-0(f.0-0(s.0(f.0-1(s.0(y_0), 0.)), s.0(f.0-1(s.0(y_1), s.1(y_2)))), f.0-0(x2, x3)) → F.0-0(f.0-1(s.0(y_0), 0.), f.0-1(s.0(y_1), s.1(y_2)))
F.0-0(f.0-0(s.0(f.1-1(s.1(y_0), 0.)), s.0(f.1-1(s.1(s.1(y_1)), s.1(s.1(y_2))))), f.1-0(x2, x3)) → F.0-0(f.1-1(s.1(y_0), 0.), f.1-1(s.1(s.1(y_1)), s.1(s.1(y_2))))
F.0-0(f.1-1(s.1(x0), 0.), f.1-0(s.1(s.1(y_0)), s.0(s.0(y_1)))) → F.0-0(f.1-0(s.1(s.1(y_0)), s.0(s.0(y_1))), f.1-0(s.1(s.1(y_0)), s.0(s.0(s.0(y_1)))))
F.0-0(f.0-0(s.0(f.0-1(s.0(y_0), 0.)), s.0(f.1-1(s.1(s.1(y_1)), s.1(0.)))), f.0-1(x2, x3)) → F.0-0(f.0-1(s.0(y_0), 0.), f.1-1(s.1(s.1(y_1)), s.1(0.)))
F.0-0(f.0-0(s.0(f.0-1(s.0(y_0), 0.)), s.0(f.0-1(s.0(y_1), s.1(y_2)))), f.1-1(x2, x3)) → F.0-0(f.0-1(s.0(y_0), 0.), f.0-1(s.0(y_1), s.1(y_2)))
F.0-0(f.0-0(s.0(f.1-1(s.1(y_0), 0.)), s.0(f.1-1(s.1(s.1(y_1)), s.1(0.)))), f.0-0(x2, x3)) → F.0-0(f.1-1(s.1(y_0), 0.), f.1-1(s.1(s.1(y_1)), s.1(0.)))
F.0-0(f.0-0(s.0(f.1-1(s.1(y_0), 0.)), s.0(f.0-1(s.0(y_1), s.1(y_2)))), f.1-0(x2, x3)) → F.0-0(f.1-1(s.1(y_0), 0.), f.0-1(s.0(y_1), s.1(y_2)))
F.0-0(f.0-0(s.0(f.0-1(s.0(y_0), 0.)), s.0(f.1-1(s.1(y_1), s.1(y_2)))), f.1-0(x2, x3)) → F.0-0(f.0-1(s.0(y_0), 0.), f.1-1(s.1(y_1), s.1(y_2)))
F.0-0(f.0-0(s.0(f.0-1(s.0(y_0), s.1(y_1))), s.0(x1)), f.0-0(x2, x3)) → F.0-0(f.0-1(s.0(y_0), s.1(y_1)), x1)
F.0-0(f.1-1(s.1(s.1(y_0)), s.1(0.)), f.1-1(x2, x3)) → F.0-0(f.1-1(s.1(y_0), 0.), f.1-1(x2, x3))
F.0-0(f.0-0(s.0(f.1-1(s.1(y_0), 0.)), s.0(f.1-1(s.1(s.1(y_1)), s.1(s.1(y_2))))), f.1-1(x2, x3)) → F.0-0(f.1-1(s.1(y_0), 0.), f.1-1(s.1(s.1(y_1)), s.1(s.1(y_2))))
F.0-0(f.0-0(s.0(f.0-1(s.0(y_0), 0.)), s.0(f.1-1(s.1(s.1(y_1)), s.1(0.)))), f.1-0(x2, x3)) → F.0-0(f.0-1(s.0(y_0), 0.), f.1-1(s.1(s.1(y_1)), s.1(0.)))
F.0-0(f.0-1(s.0(x0), 0.), f.1-1(s.1(s.1(y_0)), s.1(s.1(y_1)))) → F.0-0(f.1-1(s.1(s.1(y_0)), s.1(s.1(y_1))), f.1-1(s.1(s.1(y_0)), s.1(s.1(s.1(y_1)))))
F.0-0(f.0-0(s.0(f.0-1(s.0(s.0(y_0)), s.1(0.))), s.0(x1)), f.1-0(x2, x3)) → F.0-0(f.0-1(s.0(s.0(y_0)), s.1(0.)), x1)
F.0-0(f.0-0(s.0(f.1-1(s.1(s.1(y_0)), s.1(0.))), s.0(x1)), f.1-0(x2, x3)) → F.0-0(f.1-1(s.1(s.1(y_0)), s.1(0.)), x1)
F.0-0(f.0-0(s.0(f.1-1(s.1(y_0), 0.)), s.0(f.0-0(s.0(y_1), s.0(y_2)))), f.0-0(x2, x3)) → F.0-0(f.1-1(s.1(y_0), 0.), f.0-0(s.0(y_1), s.0(y_2)))
F.0-0(f.0-0(s.0(f.0-1(s.0(y_0), 0.)), s.0(f.1-0(s.1(y_1), s.0(y_2)))), f.0-0(x2, x3)) → F.0-0(f.0-1(s.0(y_0), 0.), f.1-0(s.1(y_1), s.0(y_2)))
F.0-0(f.0-0(s.0(f.0-1(s.0(y_0), 0.)), s.0(f.0-1(s.0(s.0(y_1)), s.1(s.1(y_2))))), f.1-0(x2, x3)) → F.0-0(f.0-1(s.0(y_0), 0.), f.0-1(s.0(s.0(y_1)), s.1(s.1(y_2))))
F.0-0(f.1-1(s.1(x0), 0.), f.1-1(s.1(y_0), s.1(y_1))) → F.0-0(f.1-1(s.1(y_0), s.1(y_1)), f.1-1(s.1(y_0), s.1(s.1(y_1))))
F.0-0(f.0-1(s.0(f.0-0(s.0(s.0(y_0)), s.0(s.0(y_1)))), s.1(x1)), f.0-1(x2, x3)) → F.0-1(f.0-0(s.0(s.0(y_0)), s.0(s.0(y_1))), x1)
F.0-0(f.0-0(s.0(f.1-0(s.1(y_0), s.0(y_1))), s.0(x1)), f.1-1(x2, x3)) → F.0-0(f.1-0(s.1(y_0), s.0(y_1)), x1)
F.0-0(f.0-0(s.0(f.1-1(s.1(y_0), 0.)), s.0(f.1-1(s.1(y_1), 0.))), f.0-1(x2, x3)) → F.0-0(f.1-1(s.1(y_0), 0.), f.1-1(s.1(y_1), 0.))
F.0-0(f.0-0(s.0(f.0-1(s.0(y_0), 0.)), s.0(f.0-1(s.0(y_1), s.1(y_2)))), f.1-0(x2, x3)) → F.0-0(f.0-1(s.0(y_0), 0.), f.0-1(s.0(y_1), s.1(y_2)))
F.0-0(f.0-0(s.0(f.0-1(s.0(y_0), s.1(y_1))), s.0(x1)), f.1-0(x2, x3)) → F.0-0(f.0-1(s.0(y_0), s.1(y_1)), x1)
F.0-0(f.0-0(s.0(f.0-1(s.0(y_0), 0.)), s.0(f.1-1(s.1(s.1(y_1)), s.1(s.1(y_2))))), f.0-0(x2, x3)) → F.0-0(f.0-1(s.0(y_0), 0.), f.1-1(s.1(s.1(y_1)), s.1(s.1(y_2))))
F.0-0(f.0-0(s.0(f.1-0(s.1(y_0), s.0(y_1))), s.0(x1)), f.0-1(x2, x3)) → F.0-0(f.1-0(s.1(y_0), s.0(y_1)), x1)
F.0-0(f.0-0(s.0(f.0-1(s.0(y_0), 0.)), s.0(f.1-0(s.1(s.1(y_1)), s.0(s.0(y_2))))), f.1-1(x2, x3)) → F.0-0(f.0-1(s.0(y_0), 0.), f.1-0(s.1(s.1(y_1)), s.0(s.0(y_2))))
F.0-0(f.0-1(s.0(f.0-0(s.0(y_0), s.0(y_1))), s.1(x1)), f.0-0(x2, x3)) → F.0-1(f.0-0(s.0(y_0), s.0(y_1)), x1)
F.0-0(f.0-0(s.0(f.1-0(s.1(s.1(y_0)), s.0(s.0(y_1)))), s.0(x1)), f.1-1(x2, x3)) → F.0-0(f.1-0(s.1(s.1(y_0)), s.0(s.0(y_1))), x1)
F.0-0(f.0-0(s.0(f.1-0(s.1(s.1(y_0)), s.0(s.0(y_1)))), s.0(x1)), f.1-0(x2, x3)) → F.0-0(f.1-0(s.1(s.1(y_0)), s.0(s.0(y_1))), x1)
F.0-0(f.0-1(s.0(f.1-0(s.1(s.1(y_0)), s.0(s.0(y_1)))), s.1(x1)), f.0-0(x2, x3)) → F.0-1(f.1-0(s.1(s.1(y_0)), s.0(s.0(y_1))), x1)
F.0-0(f.0-1(s.0(x0), 0.), f.1-1(s.1(y_0), s.1(y_1))) → F.0-0(f.1-1(s.1(y_0), s.1(y_1)), f.1-1(s.1(y_0), s.1(s.1(y_1))))
F.0-0(f.0-0(s.0(f.0-1(s.0(y_0), 0.)), s.0(f.1-1(s.1(s.1(y_1)), s.1(0.)))), f.1-1(x2, x3)) → F.0-0(f.0-1(s.0(y_0), 0.), f.1-1(s.1(s.1(y_1)), s.1(0.)))
F.0-0(f.0-0(s.0(f.0-1(s.0(y_0), 0.)), s.0(f.0-0(s.0(s.0(y_1)), s.0(s.0(y_2))))), f.0-1(x2, x3)) → F.0-0(f.0-1(s.0(y_0), 0.), f.0-0(s.0(s.0(y_1)), s.0(s.0(y_2))))
F.0-0(f.0-1(s.0(f.1-1(s.1(s.1(y_0)), s.1(0.))), s.1(x1)), f.1-0(x2, x3)) → F.0-1(f.1-1(s.1(s.1(y_0)), s.1(0.)), x1)
F.0-0(f.0-0(s.0(f.1-1(s.1(y_0), 0.)), s.0(f.0-1(s.0(s.0(y_1)), s.1(s.1(y_2))))), f.1-1(x2, x3)) → F.0-0(f.1-1(s.1(y_0), 0.), f.0-1(s.0(s.0(y_1)), s.1(s.1(y_2))))
F.0-0(f.1-1(s.1(x0), 0.), f.0-1(s.0(y_0), 0.)) → F.0-0(f.0-1(s.0(y_0), 0.), f.0-1(s.0(y_0), s.1(0.)))
F.0-0(f.0-0(s.0(f.1-1(s.1(y_0), 0.)), s.0(f.1-0(s.1(s.1(y_1)), s.0(s.0(y_2))))), f.1-1(x2, x3)) → F.0-0(f.1-1(s.1(y_0), 0.), f.1-0(s.1(s.1(y_1)), s.0(s.0(y_2))))
F.0-0(f.0-1(s.0(f.0-0(s.0(y_0), s.0(y_1))), s.1(x1)), f.1-0(x2, x3)) → F.0-1(f.0-0(s.0(y_0), s.0(y_1)), x1)
F.0-0(f.0-0(s.0(f.1-1(s.1(y_0), 0.)), s.0(f.1-0(s.1(s.1(y_1)), s.0(s.0(y_2))))), f.0-1(x2, x3)) → F.0-0(f.1-1(s.1(y_0), 0.), f.1-0(s.1(s.1(y_1)), s.0(s.0(y_2))))
F.0-0(f.0-0(s.0(f.0-1(s.0(y_0), 0.)), s.0(f.0-0(s.0(s.0(y_1)), s.0(s.0(y_2))))), f.1-0(x2, x3)) → F.0-0(f.0-1(s.0(y_0), 0.), f.0-0(s.0(s.0(y_1)), s.0(s.0(y_2))))
F.0-0(f.0-1(s.0(f.0-1(s.0(s.0(y_0)), s.1(0.))), s.1(x1)), f.0-1(x2, x3)) → F.0-1(f.0-1(s.0(s.0(y_0)), s.1(0.)), x1)
F.0-0(f.1-1(s.1(x0), 0.), f.0-0(s.0(s.0(y_0)), s.0(s.0(y_1)))) → F.0-0(f.0-0(s.0(s.0(y_0)), s.0(s.0(y_1))), f.0-0(s.0(s.0(y_0)), s.0(s.0(s.0(y_1)))))
F.0-0(f.0-0(s.0(f.0-1(s.0(y_0), 0.)), s.0(f.0-1(s.0(s.0(y_1)), s.1(s.1(y_2))))), f.1-1(x2, x3)) → F.0-0(f.0-1(s.0(y_0), 0.), f.0-1(s.0(s.0(y_1)), s.1(s.1(y_2))))
F.0-0(f.0-1(s.0(f.1-1(s.1(s.1(y_0)), s.1(0.))), s.1(x1)), f.0-1(x2, x3)) → F.0-1(f.1-1(s.1(s.1(y_0)), s.1(0.)), x1)
F.0-0(f.0-0(s.0(f.1-1(s.1(y_0), 0.)), s.0(f.1-1(s.1(s.1(y_1)), s.1(s.1(y_2))))), f.0-0(x2, x3)) → F.0-0(f.1-1(s.1(y_0), 0.), f.1-1(s.1(s.1(y_1)), s.1(s.1(y_2))))
F.0-0(f.0-0(s.0(f.1-1(s.1(y_0), 0.)), s.0(f.0-1(s.0(s.0(y_1)), s.1(s.1(y_2))))), f.0-1(x2, x3)) → F.0-0(f.1-1(s.1(y_0), 0.), f.0-1(s.0(s.0(y_1)), s.1(s.1(y_2))))
F.0-0(f.0-1(s.0(x0), 0.), f.0-1(s.0(s.0(y_0)), s.1(s.1(y_1)))) → F.0-0(f.0-1(s.0(s.0(y_0)), s.1(s.1(y_1))), f.0-1(s.0(s.0(y_0)), s.1(s.1(s.1(y_1)))))
F.0-0(f.0-0(s.0(f.1-1(s.1(y_0), 0.)), s.0(f.1-0(s.1(y_1), s.0(y_2)))), f.0-0(x2, x3)) → F.0-0(f.1-1(s.1(y_0), 0.), f.1-0(s.1(y_1), s.0(y_2)))
F.0-0(f.0-0(s.0(f.0-1(s.0(s.0(y_0)), s.1(s.1(y_1)))), s.0(x1)), f.1-0(x2, x3)) → F.0-0(f.0-1(s.0(s.0(y_0)), s.1(s.1(y_1))), x1)
F.0-0(f.0-0(s.0(f.1-1(s.1(y_0), 0.)), s.0(f.1-0(s.1(y_1), s.0(y_2)))), f.1-1(x2, x3)) → F.0-0(f.1-1(s.1(y_0), 0.), f.1-0(s.1(y_1), s.0(y_2)))
F.0-0(f.0-0(s.0(f.1-1(s.1(y_0), 0.)), s.0(f.1-1(s.1(y_1), s.1(y_2)))), f.1-1(x2, x3)) → F.0-0(f.1-1(s.1(y_0), 0.), f.1-1(s.1(y_1), s.1(y_2)))
F.0-0(f.0-0(s.0(f.0-0(s.0(s.0(y_0)), s.0(s.0(y_1)))), s.0(x1)), f.0-1(x2, x3)) → F.0-0(f.0-0(s.0(s.0(y_0)), s.0(s.0(y_1))), x1)
F.0-0(f.0-0(s.0(f.1-1(s.1(y_0), 0.)), s.0(f.1-1(s.1(s.1(y_1)), s.1(0.)))), f.0-1(x2, x3)) → F.0-0(f.1-1(s.1(y_0), 0.), f.1-1(s.1(s.1(y_1)), s.1(0.)))
F.0-0(f.0-0(s.0(f.1-0(s.1(s.1(y_0)), s.0(s.0(y_1)))), s.0(x1)), f.0-1(x2, x3)) → F.0-0(f.1-0(s.1(s.1(y_0)), s.0(s.0(y_1))), x1)
F.0-0(f.0-0(s.0(f.1-1(s.1(y_0), 0.)), s.0(f.0-0(s.0(s.0(y_1)), s.0(s.0(y_2))))), f.1-1(x2, x3)) → F.0-0(f.1-1(s.1(y_0), 0.), f.0-0(s.0(s.0(y_1)), s.0(s.0(y_2))))
F.0-0(f.1-1(s.1(s.1(y_0)), s.1(s.1(y_1))), f.1-0(x2, x3)) → F.0-0(f.1-1(s.1(y_0), s.1(y_1)), f.1-0(x2, x3))
F.0-0(f.0-1(s.0(f.1-1(s.1(y_0), s.1(y_1))), s.1(x1)), f.0-0(x2, x3)) → F.0-1(f.1-1(s.1(y_0), s.1(y_1)), x1)
F.0-0(f.1-1(s.1(s.1(y_0)), s.1(s.1(y_1))), f.0-0(x2, x3)) → F.0-0(f.1-1(s.1(y_0), s.1(y_1)), f.0-0(x2, x3))
F.0-0(f.1-1(s.1(s.1(y_0)), s.1(0.)), f.0-0(x2, x3)) → F.0-0(f.1-1(s.1(y_0), 0.), f.0-0(x2, x3))
F.0-0(f.0-0(s.0(f.0-1(s.0(y_0), 0.)), s.0(f.0-1(s.0(s.0(y_1)), s.1(s.1(y_2))))), f.0-1(x2, x3)) → F.0-0(f.0-1(s.0(y_0), 0.), f.0-1(s.0(s.0(y_1)), s.1(s.1(y_2))))
F.0-0(f.0-1(s.0(f.1-1(s.1(s.1(y_0)), s.1(0.))), s.1(x1)), f.0-0(x2, x3)) → F.0-1(f.1-1(s.1(s.1(y_0)), s.1(0.)), x1)
F.0-0(f.0-0(s.0(f.0-1(s.0(y_0), s.1(y_1))), s.0(x1)), f.0-1(x2, x3)) → F.0-0(f.0-1(s.0(y_0), s.1(y_1)), x1)
F.0-0(f.0-1(s.0(f.1-0(s.1(s.1(y_0)), s.0(s.0(y_1)))), s.1(x1)), f.1-1(x2, x3)) → F.0-1(f.1-0(s.1(s.1(y_0)), s.0(s.0(y_1))), x1)
F.0-0(f.0-1(s.0(f.0-1(s.0(y_0), s.1(y_1))), s.1(x1)), f.1-0(x2, x3)) → F.0-1(f.0-1(s.0(y_0), s.1(y_1)), x1)
F.0-0(f.0-1(s.0(f.1-0(s.1(y_0), s.0(y_1))), s.1(x1)), f.1-1(x2, x3)) → F.0-1(f.1-0(s.1(y_0), s.0(y_1)), x1)
F.0-0(f.0-0(s.0(f.0-1(s.0(y_0), 0.)), s.0(f.1-1(s.1(s.1(y_1)), s.1(s.1(y_2))))), f.1-0(x2, x3)) → F.0-0(f.0-1(s.0(y_0), 0.), f.1-1(s.1(s.1(y_1)), s.1(s.1(y_2))))
F.0-0(f.0-0(s.0(f.1-1(s.1(y_0), s.1(y_1))), s.0(x1)), f.0-0(x2, x3)) → F.0-0(f.1-1(s.1(y_0), s.1(y_1)), x1)
F.0-0(f.0-0(s.0(f.0-1(s.0(s.0(y_0)), s.1(s.1(y_1)))), s.0(x1)), f.1-1(x2, x3)) → F.0-0(f.0-1(s.0(s.0(y_0)), s.1(s.1(y_1))), x1)
F.0-0(f.1-1(s.1(x0), 0.), f.0-1(s.0(s.0(y_0)), s.1(s.1(y_1)))) → F.0-0(f.0-1(s.0(s.0(y_0)), s.1(s.1(y_1))), f.0-1(s.0(s.0(y_0)), s.1(s.1(s.1(y_1)))))
F.0-0(f.0-0(s.0(f.1-1(s.1(y_0), 0.)), s.0(f.1-0(s.1(y_1), s.0(y_2)))), f.1-0(x2, x3)) → F.0-0(f.1-1(s.1(y_0), 0.), f.1-0(s.1(y_1), s.0(y_2)))
F.0-0(f.0-1(s.0(f.0-1(s.0(y_0), s.1(y_1))), s.1(x1)), f.0-1(x2, x3)) → F.0-1(f.0-1(s.0(y_0), s.1(y_1)), x1)
F.0-0(f.0-1(s.0(f.0-0(s.0(s.0(y_0)), s.0(s.0(y_1)))), s.1(x1)), f.0-0(x2, x3)) → F.0-1(f.0-0(s.0(s.0(y_0)), s.0(s.0(y_1))), x1)
F.0-0(f.0-0(s.0(f.1-1(s.1(s.1(y_0)), s.1(s.1(y_1)))), s.0(x1)), f.1-1(x2, x3)) → F.0-0(f.1-1(s.1(s.1(y_0)), s.1(s.1(y_1))), x1)
F.0-0(f.0-0(s.0(f.1-1(s.1(s.1(y_0)), s.1(0.))), s.0(x1)), f.0-0(x2, x3)) → F.0-0(f.1-1(s.1(s.1(y_0)), s.1(0.)), x1)
F.0-0(f.0-0(s.0(f.1-1(s.1(y_0), 0.)), s.0(f.1-0(s.1(s.1(y_1)), s.0(s.0(y_2))))), f.1-0(x2, x3)) → F.0-0(f.1-1(s.1(y_0), 0.), f.1-0(s.1(s.1(y_1)), s.0(s.0(y_2))))
F.0-0(f.0-0(s.0(f.0-0(s.0(s.0(y_0)), s.0(s.0(y_1)))), s.0(x1)), f.1-1(x2, x3)) → F.0-0(f.0-0(s.0(s.0(y_0)), s.0(s.0(y_1))), x1)
F.0-0(f.0-0(s.0(f.1-1(s.1(s.1(y_0)), s.1(0.))), s.0(x1)), f.0-1(x2, x3)) → F.0-0(f.1-1(s.1(s.1(y_0)), s.1(0.)), x1)
F.0-0(f.0-0(s.0(f.1-1(s.1(y_0), 0.)), s.0(f.0-1(s.0(y_1), s.1(y_2)))), f.0-1(x2, x3)) → F.0-0(f.1-1(s.1(y_0), 0.), f.0-1(s.0(y_1), s.1(y_2)))
F.0-0(f.0-0(s.0(f.0-1(s.0(y_0), 0.)), s.0(f.1-1(s.1(y_1), s.1(y_2)))), f.0-1(x2, x3)) → F.0-0(f.0-1(s.0(y_0), 0.), f.1-1(s.1(y_1), s.1(y_2)))
F.0-0(f.0-1(s.0(s.0(y_0)), s.1(s.1(y_1))), f.0-0(x2, x3)) → F.0-0(f.0-1(s.0(y_0), s.1(y_1)), f.0-0(x2, x3))
F.0-0(f.0-0(s.0(f.0-1(s.0(s.0(y_0)), s.1(s.1(y_1)))), s.0(x1)), f.0-1(x2, x3)) → F.0-0(f.0-1(s.0(s.0(y_0)), s.1(s.1(y_1))), x1)
F.0-0(f.0-1(s.0(f.1-1(s.1(s.1(y_0)), s.1(s.1(y_1)))), s.1(x1)), f.0-1(x2, x3)) → F.0-1(f.1-1(s.1(s.1(y_0)), s.1(s.1(y_1))), x1)
F.0-0(f.0-0(s.0(f.1-1(s.1(y_0), 0.)), s.0(f.0-1(s.0(s.0(y_1)), s.1(0.)))), f.1-1(x2, x3)) → F.0-0(f.1-1(s.1(y_0), 0.), f.0-1(s.0(s.0(y_1)), s.1(0.)))
F.0-0(f.0-0(s.0(f.1-1(s.1(y_0), 0.)), s.0(f.0-0(s.0(s.0(y_1)), s.0(s.0(y_2))))), f.1-0(x2, x3)) → F.0-0(f.1-1(s.1(y_0), 0.), f.0-0(s.0(s.0(y_1)), s.0(s.0(y_2))))
F.0-0(f.0-0(s.0(f.1-1(s.1(y_0), 0.)), s.0(f.0-0(s.0(y_1), s.0(y_2)))), f.1-0(x2, x3)) → F.0-0(f.1-1(s.1(y_0), 0.), f.0-0(s.0(y_1), s.0(y_2)))
F.0-0(f.0-0(s.0(f.0-1(s.0(y_0), 0.)), s.0(f.1-0(s.1(y_1), s.0(y_2)))), f.1-0(x2, x3)) → F.0-0(f.0-1(s.0(y_0), 0.), f.1-0(s.1(y_1), s.0(y_2)))
F.0-0(f.0-0(s.0(f.1-1(s.1(y_0), 0.)), s.0(f.0-1(s.0(s.0(y_1)), s.1(s.1(y_2))))), f.1-0(x2, x3)) → F.0-0(f.1-1(s.1(y_0), 0.), f.0-1(s.0(s.0(y_1)), s.1(s.1(y_2))))
F.0-0(f.0-0(s.0(f.0-1(s.0(s.0(y_0)), s.1(s.1(y_1)))), s.0(x1)), f.0-0(x2, x3)) → F.0-0(f.0-1(s.0(s.0(y_0)), s.1(s.1(y_1))), x1)
F.0-0(f.0-0(s.0(f.1-1(s.1(s.1(y_0)), s.1(s.1(y_1)))), s.0(x1)), f.0-0(x2, x3)) → F.0-0(f.1-1(s.1(s.1(y_0)), s.1(s.1(y_1))), x1)
F.0-0(f.0-1(s.0(x0), 0.), f.1-0(s.1(y_0), s.0(y_1))) → F.0-0(f.1-0(s.1(y_0), s.0(y_1)), f.1-0(s.1(y_0), s.0(s.0(y_1))))
F.0-0(f.0-1(s.0(x0), 0.), f.1-1(s.1(y_0), 0.)) → F.0-0(f.1-1(s.1(y_0), 0.), f.1-1(s.1(y_0), s.1(0.)))
F.0-0(f.0-1(s.0(f.1-0(s.1(s.1(y_0)), s.0(s.0(y_1)))), s.1(x1)), f.0-1(x2, x3)) → F.0-1(f.1-0(s.1(s.1(y_0)), s.0(s.0(y_1))), x1)
F.0-0(f.0-1(s.0(f.1-1(s.1(s.1(y_0)), s.1(0.))), s.1(x1)), f.1-1(x2, x3)) → F.0-1(f.1-1(s.1(s.1(y_0)), s.1(0.)), x1)
F.0-0(f.0-0(s.0(f.0-0(s.0(y_0), s.0(y_1))), s.0(x1)), f.1-1(x2, x3)) → F.0-0(f.0-0(s.0(y_0), s.0(y_1)), x1)
F.0-0(f.0-1(s.0(f.0-1(s.0(s.0(y_0)), s.1(0.))), s.1(x1)), f.1-1(x2, x3)) → F.0-1(f.0-1(s.0(s.0(y_0)), s.1(0.)), x1)
F.0-0(f.1-1(s.1(s.1(y_0)), s.1(0.)), f.1-0(x2, x3)) → F.0-0(f.1-1(s.1(y_0), 0.), f.1-0(x2, x3))
F.0-0(f.0-1(s.0(x0), 0.), f.0-1(s.0(y_0), s.1(y_1))) → F.0-0(f.0-1(s.0(y_0), s.1(y_1)), f.0-1(s.0(y_0), s.1(s.1(y_1))))
F.0-0(f.1-1(s.1(s.1(y_0)), s.1(s.1(y_1))), f.0-1(x2, x3)) → F.0-0(f.1-1(s.1(y_0), s.1(y_1)), f.0-1(x2, x3))
F.0-0(f.0-0(s.0(f.0-1(s.0(y_0), 0.)), s.0(f.1-1(s.1(s.1(y_1)), s.1(s.1(y_2))))), f.0-1(x2, x3)) → F.0-0(f.0-1(s.0(y_0), 0.), f.1-1(s.1(s.1(y_1)), s.1(s.1(y_2))))
F.0-0(f.1-1(s.1(x0), 0.), f.0-1(s.0(s.0(y_0)), s.1(0.))) → F.0-0(f.0-1(s.0(s.0(y_0)), s.1(0.)), f.0-1(s.0(s.0(y_0)), s.1(s.1(0.))))
F.0-0(f.0-1(s.0(f.0-1(s.0(y_0), s.1(y_1))), s.1(x1)), f.0-0(x2, x3)) → F.0-1(f.0-1(s.0(y_0), s.1(y_1)), x1)
F.0-0(f.0-1(s.0(f.0-0(s.0(s.0(y_0)), s.0(s.0(y_1)))), s.1(x1)), f.1-0(x2, x3)) → F.0-1(f.0-0(s.0(s.0(y_0)), s.0(s.0(y_1))), x1)
F.0-0(f.0-1(s.0(x0), 0.), f.1-1(s.1(s.1(y_0)), s.1(0.))) → F.0-0(f.1-1(s.1(s.1(y_0)), s.1(0.)), f.1-1(s.1(s.1(y_0)), s.1(s.1(0.))))
F.0-0(f.0-0(s.0(f.1-1(s.1(y_0), 0.)), s.0(f.0-1(s.0(s.0(y_1)), s.1(s.1(y_2))))), f.0-0(x2, x3)) → F.0-0(f.1-1(s.1(y_0), 0.), f.0-1(s.0(s.0(y_1)), s.1(s.1(y_2))))
F.0-0(f.0-0(s.0(f.0-1(s.0(y_0), s.1(y_1))), s.0(x1)), f.1-1(x2, x3)) → F.0-0(f.0-1(s.0(y_0), s.1(y_1)), x1)
F.0-0(f.0-0(s.0(f.0-1(s.0(y_0), 0.)), s.0(f.0-1(s.0(y_1), s.1(y_2)))), f.0-1(x2, x3)) → F.0-0(f.0-1(s.0(y_0), 0.), f.0-1(s.0(y_1), s.1(y_2)))
F.0-0(f.0-0(s.0(f.1-1(s.1(y_0), 0.)), s.0(f.1-1(s.1(s.1(y_1)), s.1(s.1(y_2))))), f.0-1(x2, x3)) → F.0-0(f.1-1(s.1(y_0), 0.), f.1-1(s.1(s.1(y_1)), s.1(s.1(y_2))))
F.0-0(f.0-1(s.0(f.1-0(s.1(y_0), s.0(y_1))), s.1(x1)), f.0-1(x2, x3)) → F.0-1(f.1-0(s.1(y_0), s.0(y_1)), x1)
F.0-0(f.0-0(s.0(f.0-1(s.0(y_0), 0.)), s.0(f.0-0(s.0(y_1), s.0(y_2)))), f.0-1(x2, x3)) → F.0-0(f.0-1(s.0(y_0), 0.), f.0-0(s.0(y_1), s.0(y_2)))
F.0-0(f.0-0(s.0(f.0-1(s.0(y_0), 0.)), s.0(f.0-1(s.0(y_1), 0.))), f.1-1(x2, x3)) → F.0-0(f.0-1(s.0(y_0), 0.), f.0-1(s.0(y_1), 0.))
F.0-0(f.0-1(s.0(f.1-0(s.1(y_0), s.0(y_1))), s.1(x1)), f.0-0(x2, x3)) → F.0-1(f.1-0(s.1(y_0), s.0(y_1)), x1)
F.0-0(f.0-0(s.0(f.1-1(s.1(y_0), 0.)), s.0(f.1-1(s.1(y_1), 0.))), f.1-1(x2, x3)) → F.0-0(f.1-1(s.1(y_0), 0.), f.1-1(s.1(y_1), 0.))
F.0-0(f.0-0(s.0(f.1-1(s.1(y_0), 0.)), s.0(f.1-1(s.1(y_1), 0.))), f.0-0(x2, x3)) → F.0-0(f.1-1(s.1(y_0), 0.), f.1-1(s.1(y_1), 0.))
F.0-0(f.0-1(s.0(s.0(y_0)), s.1(0.)), f.1-0(x2, x3)) → F.0-0(f.0-1(s.0(y_0), 0.), f.1-0(x2, x3))
F.0-0(f.0-1(s.0(f.1-0(s.1(s.1(y_0)), s.0(s.0(y_1)))), s.1(x1)), f.1-0(x2, x3)) → F.0-1(f.1-0(s.1(s.1(y_0)), s.0(s.0(y_1))), x1)
F.0-0(f.0-1(s.0(s.0(y_0)), s.1(s.1(y_1))), f.1-1(x2, x3)) → F.0-0(f.0-1(s.0(y_0), s.1(y_1)), f.1-1(x2, x3))
F.0-0(f.0-1(s.0(x0), 0.), f.0-0(s.0(s.0(y_0)), s.0(s.0(y_1)))) → F.0-0(f.0-0(s.0(s.0(y_0)), s.0(s.0(y_1))), f.0-0(s.0(s.0(y_0)), s.0(s.0(s.0(y_1)))))
F.0-0(f.0-0(s.0(f.0-1(s.0(y_0), 0.)), s.0(f.1-1(s.1(s.1(y_1)), s.1(0.)))), f.0-0(x2, x3)) → F.0-0(f.0-1(s.0(y_0), 0.), f.1-1(s.1(s.1(y_1)), s.1(0.)))
F.0-0(f.0-0(s.0(f.1-1(s.1(y_0), 0.)), s.0(f.1-1(s.1(y_1), 0.))), f.1-0(x2, x3)) → F.0-0(f.1-1(s.1(y_0), 0.), f.1-1(s.1(y_1), 0.))
F.0-0(f.0-1(s.0(f.1-1(s.1(s.1(y_0)), s.1(s.1(y_1)))), s.1(x1)), f.1-0(x2, x3)) → F.0-1(f.1-1(s.1(s.1(y_0)), s.1(s.1(y_1))), x1)
F.0-0(f.0-0(s.0(f.1-1(s.1(y_0), 0.)), s.0(f.1-1(s.1(y_1), s.1(y_2)))), f.0-0(x2, x3)) → F.0-0(f.1-1(s.1(y_0), 0.), f.1-1(s.1(y_1), s.1(y_2)))
F.0-0(f.0-0(s.0(f.1-1(s.1(y_0), 0.)), s.0(f.0-1(s.0(s.0(y_1)), s.1(0.)))), f.0-0(x2, x3)) → F.0-0(f.1-1(s.1(y_0), 0.), f.0-1(s.0(s.0(y_1)), s.1(0.)))
F.0-0(f.0-0(s.0(f.0-0(s.0(y_0), s.0(y_1))), s.0(x1)), f.1-0(x2, x3)) → F.0-0(f.0-0(s.0(y_0), s.0(y_1)), x1)
F.0-0(f.0-1(s.0(f.0-0(s.0(y_0), s.0(y_1))), s.1(x1)), f.0-1(x2, x3)) → F.0-1(f.0-0(s.0(y_0), s.0(y_1)), x1)
F.0-0(f.0-1(s.0(f.0-1(s.0(s.0(y_0)), s.1(s.1(y_1)))), s.1(x1)), f.0-1(x2, x3)) → F.0-1(f.0-1(s.0(s.0(y_0)), s.1(s.1(y_1))), x1)
F.0-0(f.0-0(s.0(f.0-1(s.0(y_0), 0.)), s.0(f.1-0(s.1(s.1(y_1)), s.0(s.0(y_2))))), f.0-1(x2, x3)) → F.0-0(f.0-1(s.0(y_0), 0.), f.1-0(s.1(s.1(y_1)), s.0(s.0(y_2))))
F.0-0(f.0-1(s.0(f.0-1(s.0(s.0(y_0)), s.1(0.))), s.1(x1)), f.0-0(x2, x3)) → F.0-1(f.0-1(s.0(s.0(y_0)), s.1(0.)), x1)
F.0-0(f.0-0(s.0(f.1-1(s.1(y_0), 0.)), s.0(f.1-1(s.1(s.1(y_1)), s.1(0.)))), f.1-1(x2, x3)) → F.0-0(f.1-1(s.1(y_0), 0.), f.1-1(s.1(s.1(y_1)), s.1(0.)))
F.0-0(f.0-0(s.0(f.0-1(s.0(y_0), 0.)), s.0(f.0-0(s.0(s.0(y_1)), s.0(s.0(y_2))))), f.1-1(x2, x3)) → F.0-0(f.0-1(s.0(y_0), 0.), f.0-0(s.0(s.0(y_1)), s.0(s.0(y_2))))
F.0-0(f.0-1(s.0(x0), 0.), f.0-1(s.0(y_0), 0.)) → F.0-0(f.0-1(s.0(y_0), 0.), f.0-1(s.0(y_0), s.1(0.)))
F.0-0(f.0-0(s.0(f.1-1(s.1(y_0), s.1(y_1))), s.0(x1)), f.0-1(x2, x3)) → F.0-0(f.1-1(s.1(y_0), s.1(y_1)), x1)
F.0-0(f.0-0(s.0(f.1-1(s.1(y_0), 0.)), s.0(f.1-1(s.1(y_1), s.1(y_2)))), f.0-1(x2, x3)) → F.0-0(f.1-1(s.1(y_0), 0.), f.1-1(s.1(y_1), s.1(y_2)))
F.0-0(f.0-0(s.0(f.1-1(s.1(s.1(y_0)), s.1(s.1(y_1)))), s.0(x1)), f.0-1(x2, x3)) → F.0-0(f.1-1(s.1(s.1(y_0)), s.1(s.1(y_1))), x1)
F.0-0(f.0-0(s.0(f.1-1(s.1(y_0), 0.)), s.0(f.0-0(s.0(s.0(y_1)), s.0(s.0(y_2))))), f.0-1(x2, x3)) → F.0-0(f.1-1(s.1(y_0), 0.), f.0-0(s.0(s.0(y_1)), s.0(s.0(y_2))))
F.0-0(f.0-1(s.0(f.1-1(s.1(y_0), s.1(y_1))), s.1(x1)), f.1-1(x2, x3)) → F.0-1(f.1-1(s.1(y_0), s.1(y_1)), x1)
F.0-0(f.0-0(s.0(f.0-0(s.0(s.0(y_0)), s.0(s.0(y_1)))), s.0(x1)), f.0-0(x2, x3)) → F.0-0(f.0-0(s.0(s.0(y_0)), s.0(s.0(y_1))), x1)
F.0-0(f.0-0(s.0(f.0-1(s.0(y_0), 0.)), s.0(f.1-1(s.1(y_1), 0.))), f.1-1(x2, x3)) → F.0-0(f.0-1(s.0(y_0), 0.), f.1-1(s.1(y_1), 0.))
F.0-0(f.0-0(s.0(f.1-1(s.1(y_0), 0.)), s.0(f.0-1(s.0(y_1), 0.))), f.1-1(x2, x3)) → F.0-0(f.1-1(s.1(y_0), 0.), f.0-1(s.0(y_1), 0.))
F.0-0(f.0-1(s.0(f.0-0(s.0(y_0), s.0(y_1))), s.1(x1)), f.1-1(x2, x3)) → F.0-1(f.0-0(s.0(y_0), s.0(y_1)), x1)
F.0-0(f.0-0(s.0(f.1-1(s.1(y_0), 0.)), s.0(f.1-1(s.1(y_1), s.1(y_2)))), f.1-0(x2, x3)) → F.0-0(f.1-1(s.1(y_0), 0.), f.1-1(s.1(y_1), s.1(y_2)))
F.0-0(f.0-0(s.0(f.1-1(s.1(y_0), 0.)), s.0(f.0-1(s.0(s.0(y_1)), s.1(0.)))), f.0-1(x2, x3)) → F.0-0(f.1-1(s.1(y_0), 0.), f.0-1(s.0(s.0(y_1)), s.1(0.)))
F.0-0(f.0-0(s.0(f.1-1(s.1(y_0), 0.)), s.0(f.0-1(s.0(y_1), s.1(y_2)))), f.1-1(x2, x3)) → F.0-0(f.1-1(s.1(y_0), 0.), f.0-1(s.0(y_1), s.1(y_2)))
F.0-0(f.0-0(s.0(f.0-1(s.0(y_0), 0.)), s.0(f.1-1(s.1(y_1), s.1(y_2)))), f.1-1(x2, x3)) → F.0-0(f.0-1(s.0(y_0), 0.), f.1-1(s.1(y_1), s.1(y_2)))
F.0-0(f.0-0(s.0(f.0-1(s.0(y_0), 0.)), s.0(f.0-0(s.0(s.0(y_1)), s.0(s.0(y_2))))), f.0-0(x2, x3)) → F.0-0(f.0-1(s.0(y_0), 0.), f.0-0(s.0(s.0(y_1)), s.0(s.0(y_2))))
F.0-0(f.0-1(s.0(x0), 0.), f.0-1(s.0(s.0(y_0)), s.1(0.))) → F.0-0(f.0-1(s.0(s.0(y_0)), s.1(0.)), f.0-1(s.0(s.0(y_0)), s.1(s.1(0.))))
F.0-0(f.0-1(s.0(f.0-1(s.0(s.0(y_0)), s.1(0.))), s.1(x1)), f.1-0(x2, x3)) → F.0-1(f.0-1(s.0(s.0(y_0)), s.1(0.)), x1)
F.0-0(f.0-0(s.0(f.0-1(s.0(y_0), 0.)), s.0(f.0-1(s.0(s.0(y_1)), s.1(s.1(y_2))))), f.0-0(x2, x3)) → F.0-0(f.0-1(s.0(y_0), 0.), f.0-1(s.0(s.0(y_1)), s.1(s.1(y_2))))
F.0-0(f.0-1(s.0(f.0-1(s.0(s.0(y_0)), s.1(s.1(y_1)))), s.1(x1)), f.1-0(x2, x3)) → F.0-1(f.0-1(s.0(s.0(y_0)), s.1(s.1(y_1))), x1)
F.0-0(f.0-1(s.0(f.0-1(s.0(s.0(y_0)), s.1(s.1(y_1)))), s.1(x1)), f.1-1(x2, x3)) → F.0-1(f.0-1(s.0(s.0(y_0)), s.1(s.1(y_1))), x1)
F.0-0(f.0-0(s.0(f.1-1(s.1(y_0), 0.)), s.0(f.1-1(s.1(s.1(y_1)), s.1(0.)))), f.1-0(x2, x3)) → F.0-0(f.1-1(s.1(y_0), 0.), f.1-1(s.1(s.1(y_1)), s.1(0.)))
F.0-0(f.0-1(s.0(f.0-1(s.0(s.0(y_0)), s.1(s.1(y_1)))), s.1(x1)), f.0-0(x2, x3)) → F.0-1(f.0-1(s.0(s.0(y_0)), s.1(s.1(y_1))), x1)
F.0-0(f.0-0(s.0(f.0-0(s.0(y_0), s.0(y_1))), s.0(x1)), f.0-0(x2, x3)) → F.0-0(f.0-0(s.0(y_0), s.0(y_1)), x1)
F.0-0(f.0-1(s.0(f.0-1(s.0(y_0), s.1(y_1))), s.1(x1)), f.1-1(x2, x3)) → F.0-1(f.0-1(s.0(y_0), s.1(y_1)), x1)
F.0-0(f.1-1(s.1(x0), 0.), f.1-1(s.1(s.1(y_0)), s.1(s.1(y_1)))) → F.0-0(f.1-1(s.1(s.1(y_0)), s.1(s.1(y_1))), f.1-1(s.1(s.1(y_0)), s.1(s.1(s.1(y_1)))))
F.0-0(f.0-0(s.0(f.1-1(s.1(y_0), 0.)), s.0(f.1-0(s.1(s.1(y_1)), s.0(s.0(y_2))))), f.0-0(x2, x3)) → F.0-0(f.1-1(s.1(y_0), 0.), f.1-0(s.1(s.1(y_1)), s.0(s.0(y_2))))
F.0-0(f.1-1(s.1(x0), 0.), f.0-1(s.0(y_0), s.1(y_1))) → F.0-0(f.0-1(s.0(y_0), s.1(y_1)), f.0-1(s.0(y_0), s.1(s.1(y_1))))
F.0-0(f.0-0(s.0(f.1-1(s.1(y_0), 0.)), s.0(f.1-0(s.1(y_1), s.0(y_2)))), f.0-1(x2, x3)) → F.0-0(f.1-1(s.1(y_0), 0.), f.1-0(s.1(y_1), s.0(y_2)))
F.0-0(f.1-1(s.1(x0), 0.), f.1-0(s.1(y_0), s.0(y_1))) → F.0-0(f.1-0(s.1(y_0), s.0(y_1)), f.1-0(s.1(y_0), s.0(s.0(y_1))))
F.0-0(f.1-1(s.1(s.1(y_0)), s.1(0.)), f.0-1(x2, x3)) → F.0-0(f.1-1(s.1(y_0), 0.), f.0-1(x2, x3))
F.0-0(f.1-1(s.1(x0), 0.), f.1-1(s.1(y_0), 0.)) → F.0-0(f.1-1(s.1(y_0), 0.), f.1-1(s.1(y_0), s.1(0.)))
F.0-0(f.0-0(s.0(f.1-1(s.1(y_0), s.1(y_1))), s.0(x1)), f.1-0(x2, x3)) → F.0-0(f.1-1(s.1(y_0), s.1(y_1)), x1)
F.0-0(f.0-0(s.0(f.1-0(s.1(y_0), s.0(y_1))), s.0(x1)), f.1-0(x2, x3)) → F.0-0(f.1-0(s.1(y_0), s.0(y_1)), x1)
F.0-0(f.0-0(s.0(f.0-1(s.0(y_0), 0.)), s.0(f.1-1(s.1(s.1(y_1)), s.1(s.1(y_2))))), f.1-1(x2, x3)) → F.0-0(f.0-1(s.0(y_0), 0.), f.1-1(s.1(s.1(y_1)), s.1(s.1(y_2))))
F.0-0(f.0-1(s.0(f.1-1(s.1(s.1(y_0)), s.1(s.1(y_1)))), s.1(x1)), f.0-0(x2, x3)) → F.0-1(f.1-1(s.1(s.1(y_0)), s.1(s.1(y_1))), x1)
F.0-0(f.0-0(s.0(s.0(y_0)), s.0(s.0(y_1))), f.0-1(x2, x3)) → F.0-0(f.0-0(s.0(y_0), s.0(y_1)), f.0-1(x2, x3))
F.0-0(f.0-1(s.0(x0), 0.), f.1-0(s.1(s.1(y_0)), s.0(s.0(y_1)))) → F.0-0(f.1-0(s.1(s.1(y_0)), s.0(s.0(y_1))), f.1-0(s.1(s.1(y_0)), s.0(s.0(s.0(y_1)))))
F.0-0(f.1-1(s.1(x0), 0.), f.1-1(s.1(s.1(y_0)), s.1(0.))) → F.0-0(f.1-1(s.1(s.1(y_0)), s.1(0.)), f.1-1(s.1(s.1(y_0)), s.1(s.1(0.))))
F.0-0(f.0-1(s.0(f.0-0(s.0(s.0(y_0)), s.0(s.0(y_1)))), s.1(x1)), f.1-1(x2, x3)) → F.0-1(f.0-0(s.0(s.0(y_0)), s.0(s.0(y_1))), x1)
F.0-0(f.1-0(s.1(s.1(y_0)), s.0(s.0(y_1))), f.0-0(x2, x3)) → F.0-0(f.1-0(s.1(y_0), s.0(y_1)), f.0-0(x2, x3))
F.0-0(f.1-0(s.1(s.1(y_0)), s.0(s.0(y_1))), f.1-0(x2, x3)) → F.0-0(f.1-0(s.1(y_0), s.0(y_1)), f.1-0(x2, x3))
F.0-0(f.0-0(s.0(s.0(y_0)), s.0(s.0(y_1))), f.0-0(x2, x3)) → F.0-0(f.0-0(s.0(y_0), s.0(y_1)), f.0-0(x2, x3))
F.0-0(f.0-0(s.0(f.0-1(s.0(s.0(y_0)), s.1(0.))), s.0(x1)), f.1-1(x2, x3)) → F.0-0(f.0-1(s.0(s.0(y_0)), s.1(0.)), x1)
F.0-0(f.1-1(s.1(s.1(y_0)), s.1(s.1(y_1))), f.1-1(x2, x3)) → F.0-0(f.1-1(s.1(y_0), s.1(y_1)), f.1-1(x2, x3))
F.0-0(f.0-0(s.0(s.0(y_0)), s.0(s.0(y_1))), f.1-1(x2, x3)) → F.0-0(f.0-0(s.0(y_0), s.0(y_1)), f.1-1(x2, x3))
F.0-0(f.0-1(s.0(x0), 0.), f.0-0(s.0(y_0), s.0(y_1))) → F.0-0(f.0-0(s.0(y_0), s.0(y_1)), f.0-0(s.0(y_0), s.0(s.0(y_1))))
F.0-0(f.1-0(s.1(s.1(y_0)), s.0(s.0(y_1))), f.1-1(x2, x3)) → F.0-0(f.1-0(s.1(y_0), s.0(y_1)), f.1-1(x2, x3))
F.0-0(f.0-1(s.0(f.1-1(s.1(y_0), s.1(y_1))), s.1(x1)), f.1-0(x2, x3)) → F.0-1(f.1-1(s.1(y_0), s.1(y_1)), x1)
F.0-0(f.0-0(s.0(f.0-1(s.0(y_0), 0.)), s.0(f.1-1(s.1(y_1), 0.))), f.0-1(x2, x3)) → F.0-0(f.0-1(s.0(y_0), 0.), f.1-1(s.1(y_1), 0.))
F.0-0(f.0-0(s.0(f.1-1(s.1(y_0), 0.)), s.0(f.0-1(s.0(y_1), 0.))), f.0-1(x2, x3)) → F.0-0(f.1-1(s.1(y_0), 0.), f.0-1(s.0(y_1), 0.))
F.0-0(f.0-0(s.0(f.1-1(s.1(s.1(y_0)), s.1(s.1(y_1)))), s.0(x1)), f.1-0(x2, x3)) → F.0-0(f.1-1(s.1(s.1(y_0)), s.1(s.1(y_1))), x1)
F.0-0(f.0-0(s.0(f.1-1(s.1(y_0), 0.)), s.0(f.0-1(s.0(s.0(y_1)), s.1(0.)))), f.1-0(x2, x3)) → F.0-0(f.1-1(s.1(y_0), 0.), f.0-1(s.0(s.0(y_1)), s.1(0.)))
F.0-0(f.0-0(s.0(f.1-0(s.1(s.1(y_0)), s.0(s.0(y_1)))), s.0(x1)), f.0-0(x2, x3)) → F.0-0(f.1-0(s.1(s.1(y_0)), s.0(s.0(y_1))), x1)
F.0-0(f.0-0(s.0(f.1-1(s.1(y_0), 0.)), s.0(f.0-0(s.0(y_1), s.0(y_2)))), f.1-1(x2, x3)) → F.0-0(f.1-1(s.1(y_0), 0.), f.0-0(s.0(y_1), s.0(y_2)))
F.0-0(f.0-0(s.0(f.0-1(s.0(y_0), 0.)), s.0(f.1-0(s.1(y_1), s.0(y_2)))), f.1-1(x2, x3)) → F.0-0(f.0-1(s.0(y_0), 0.), f.1-0(s.1(y_1), s.0(y_2)))
F.0-0(f.0-0(s.0(f.0-0(s.0(y_0), s.0(y_1))), s.0(x1)), f.0-1(x2, x3)) → F.0-0(f.0-0(s.0(y_0), s.0(y_1)), x1)
F.0-0(f.0-0(s.0(f.0-1(s.0(s.0(y_0)), s.1(0.))), s.0(x1)), f.0-1(x2, x3)) → F.0-0(f.0-1(s.0(s.0(y_0)), s.1(0.)), x1)
F.0-0(f.0-0(s.0(s.0(y_0)), s.0(s.0(y_1))), f.1-0(x2, x3)) → F.0-0(f.0-0(s.0(y_0), s.0(y_1)), f.1-0(x2, x3))
F.0-0(f.0-1(s.0(s.0(y_0)), s.1(0.)), f.0-1(x2, x3)) → F.0-0(f.0-1(s.0(y_0), 0.), f.0-1(x2, x3))
F.0-0(f.0-1(s.0(s.0(y_0)), s.1(s.1(y_1))), f.0-1(x2, x3)) → F.0-0(f.0-1(s.0(y_0), s.1(y_1)), f.0-1(x2, x3))
F.0-0(f.0-0(s.0(f.0-1(s.0(y_0), 0.)), s.0(f.0-1(s.0(s.0(y_1)), s.1(0.)))), f.0-0(x2, x3)) → F.0-0(f.0-1(s.0(y_0), 0.), f.0-1(s.0(s.0(y_1)), s.1(0.)))
F.0-0(f.1-1(s.1(x0), 0.), f.0-0(s.0(y_0), s.0(y_1))) → F.0-0(f.0-0(s.0(y_0), s.0(y_1)), f.0-0(s.0(y_0), s.0(s.0(y_1))))
F.0-0(f.0-0(s.0(f.1-1(s.1(y_0), s.1(y_1))), s.0(x1)), f.1-1(x2, x3)) → F.0-0(f.1-1(s.1(y_0), s.1(y_1)), x1)
F.0-0(f.0-0(s.0(f.0-1(s.0(s.0(y_0)), s.1(0.))), s.0(x1)), f.0-0(x2, x3)) → F.0-0(f.0-1(s.0(s.0(y_0)), s.1(0.)), x1)
F.0-0(f.0-0(s.0(f.1-1(s.1(y_0), 0.)), s.0(f.0-0(s.0(s.0(y_1)), s.0(s.0(y_2))))), f.0-0(x2, x3)) → F.0-0(f.1-1(s.1(y_0), 0.), f.0-0(s.0(s.0(y_1)), s.0(s.0(y_2))))
F.0-0(f.0-1(s.0(f.1-1(s.1(y_0), s.1(y_1))), s.1(x1)), f.0-1(x2, x3)) → F.0-1(f.1-1(s.1(y_0), s.1(y_1)), x1)
F.0-0(f.0-0(s.0(f.0-1(s.0(y_0), 0.)), s.0(f.1-1(s.1(y_1), 0.))), f.0-0(x2, x3)) → F.0-0(f.0-1(s.0(y_0), 0.), f.1-1(s.1(y_1), 0.))
F.0-0(f.0-0(s.0(f.1-1(s.1(y_0), 0.)), s.0(f.0-1(s.0(y_1), 0.))), f.0-0(x2, x3)) → F.0-0(f.1-1(s.1(y_0), 0.), f.0-1(s.0(y_1), 0.))
F.0-0(f.0-1(s.0(f.1-1(s.1(s.1(y_0)), s.1(s.1(y_1)))), s.1(x1)), f.1-1(x2, x3)) → F.0-1(f.1-1(s.1(s.1(y_0)), s.1(s.1(y_1))), x1)
F.0-0(f.0-0(s.0(f.0-0(s.0(s.0(y_0)), s.0(s.0(y_1)))), s.0(x1)), f.1-0(x2, x3)) → F.0-0(f.0-0(s.0(s.0(y_0)), s.0(s.0(y_1))), x1)
F.0-0(f.0-1(s.0(s.0(y_0)), s.1(0.)), f.1-1(x2, x3)) → F.0-0(f.0-1(s.0(y_0), 0.), f.1-1(x2, x3))
F.0-0(f.0-1(s.0(s.0(y_0)), s.1(s.1(y_1))), f.1-0(x2, x3)) → F.0-0(f.0-1(s.0(y_0), s.1(y_1)), f.1-0(x2, x3))
F.0-0(f.1-0(s.1(s.1(y_0)), s.0(s.0(y_1))), f.0-1(x2, x3)) → F.0-0(f.1-0(s.1(y_0), s.0(y_1)), f.0-1(x2, x3))
F.0-0(f.0-0(s.0(f.1-1(s.1(y_0), 0.)), s.0(f.0-0(s.0(y_1), s.0(y_2)))), f.0-1(x2, x3)) → F.0-0(f.1-1(s.1(y_0), 0.), f.0-0(s.0(y_1), s.0(y_2)))
F.0-0(f.0-0(s.0(f.0-1(s.0(y_0), 0.)), s.0(f.1-0(s.1(y_1), s.0(y_2)))), f.0-1(x2, x3)) → F.0-0(f.0-1(s.0(y_0), 0.), f.1-0(s.1(y_1), s.0(y_2)))
F.0-0(f.0-0(s.0(f.0-1(s.0(y_0), 0.)), s.0(f.0-1(s.0(y_1), 0.))), f.1-0(x2, x3)) → F.0-0(f.0-1(s.0(y_0), 0.), f.0-1(s.0(y_1), 0.))
F.0-0(f.0-0(s.0(f.0-1(s.0(y_0), 0.)), s.0(f.0-1(s.0(s.0(y_1)), s.1(0.)))), f.1-1(x2, x3)) → F.0-0(f.0-1(s.0(y_0), 0.), f.0-1(s.0(s.0(y_1)), s.1(0.)))
F.0-0(f.0-0(s.0(f.0-1(s.0(y_0), 0.)), s.0(f.0-1(s.0(y_1), 0.))), f.0-0(x2, x3)) → F.0-0(f.0-1(s.0(y_0), 0.), f.0-1(s.0(y_1), 0.))
F.0-0(f.0-0(s.0(f.0-1(s.0(y_0), 0.)), s.0(f.1-0(s.1(s.1(y_1)), s.0(s.0(y_2))))), f.0-0(x2, x3)) → F.0-0(f.0-1(s.0(y_0), 0.), f.1-0(s.1(s.1(y_1)), s.0(s.0(y_2))))
f.0-0(f.0-0(s.0(x), s.0(y)), f.1-0(z, w)) → f.0-0(f.0-0(x, y), f.1-0(z, w))
f.0-0(f.1-1(s.1(x), s.1(y)), f.1-0(z, w)) → f.0-0(f.1-1(x, y), f.1-0(z, w))
f.0-0(f.0-1(s.0(x), s.1(y)), f.0-1(z, w)) → f.0-0(f.0-1(x, y), f.0-1(z, w))
f.0-0(f.0-0(s.0(x), s.0(y)), f.0-1(z, w)) → f.0-0(f.0-0(x, y), f.0-1(z, w))
f.0-0(f.0-1(s.0(x), 0.), f.1-1(y, z)) → f.0-0(f.1-1(y, z), f.1-1(y, s.1(z)))
f.0-0(f.1-1(s.1(x), 0.), f.0-1(y, z)) → f.0-0(f.0-1(y, z), f.0-1(y, s.1(z)))
f.0-0(f.1-1(s.1(x), s.1(y)), f.0-1(z, w)) → f.0-0(f.1-1(x, y), f.0-1(z, w))
f.0-0(f.1-1(s.1(x), s.1(y)), f.0-0(z, w)) → f.0-0(f.1-1(x, y), f.0-0(z, w))
f.0-0(f.0-0(s.0(x), s.0(y)), f.1-1(z, w)) → f.0-0(f.0-0(x, y), f.1-1(z, w))
f.0-0(f.0-1(s.0(x), 0.), f.0-0(y, z)) → f.0-0(f.0-0(y, z), f.0-0(y, s.0(z)))
f.0-0(f.1-1(s.1(x), 0.), f.0-0(y, z)) → f.0-0(f.0-0(y, z), f.0-0(y, s.0(z)))
f.0-0(f.0-1(s.0(x), 0.), f.0-1(y, z)) → f.0-0(f.0-1(y, z), f.0-1(y, s.1(z)))
f.0-0(f.1-1(s.1(x), s.1(y)), f.1-1(z, w)) → f.0-0(f.1-1(x, y), f.1-1(z, w))
f.0-0(f.0-0(s.0(x), s.0(y)), f.0-0(z, w)) → f.0-0(f.0-0(x, y), f.0-0(z, w))
f.0-0(f.1-1(s.1(x), 0.), f.1-0(y, z)) → f.0-0(f.1-0(y, z), f.1-0(y, s.0(z)))
f.0-0(f.0-1(s.0(x), s.1(y)), f.0-0(z, w)) → f.0-0(f.0-1(x, y), f.0-0(z, w))
f.0-0(f.1-0(s.1(x), s.0(y)), f.1-0(z, w)) → f.0-0(f.1-0(x, y), f.1-0(z, w))
f.0-0(f.1-0(s.1(x), s.0(y)), f.0-1(z, w)) → f.0-0(f.1-0(x, y), f.0-1(z, w))
f.0-0(f.0-1(s.0(x), s.1(y)), f.1-0(z, w)) → f.0-0(f.0-1(x, y), f.1-0(z, w))
f.0-0(f.0-1(s.0(x), s.1(y)), f.1-1(z, w)) → f.0-0(f.0-1(x, y), f.1-1(z, w))
f.0-0(f.1-1(s.1(x), 0.), f.1-1(y, z)) → f.0-0(f.1-1(y, z), f.1-1(y, s.1(z)))
f.0-0(f.1-0(s.1(x), s.0(y)), f.0-0(z, w)) → f.0-0(f.1-0(x, y), f.0-0(z, w))
f.0-0(f.0-1(s.0(x), 0.), f.1-0(y, z)) → f.0-0(f.1-0(y, z), f.1-0(y, s.0(z)))
f.0-0(f.1-0(s.1(x), s.0(y)), f.1-1(z, w)) → f.0-0(f.1-0(x, y), f.1-1(z, w))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ SemLabProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesReductionPairsProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ SemLabProof2
F.0-0(f.1-0(s.1(s.1(y_0)), s.0(s.0(y_1))), f.1-1(x2, x3)) → F.0-0(f.1-0(s.1(y_0), s.0(y_1)), f.1-1(x2, x3))
f.0-0(f.0-0(s.0(x), s.0(y)), f.1-0(z, w)) → f.0-0(f.0-0(x, y), f.1-0(z, w))
f.0-0(f.1-1(s.1(x), s.1(y)), f.1-0(z, w)) → f.0-0(f.1-1(x, y), f.1-0(z, w))
f.0-0(f.0-1(s.0(x), s.1(y)), f.0-1(z, w)) → f.0-0(f.0-1(x, y), f.0-1(z, w))
f.0-0(f.0-0(s.0(x), s.0(y)), f.0-1(z, w)) → f.0-0(f.0-0(x, y), f.0-1(z, w))
f.0-0(f.0-1(s.0(x), 0.), f.1-1(y, z)) → f.0-0(f.1-1(y, z), f.1-1(y, s.1(z)))
f.0-0(f.1-1(s.1(x), 0.), f.0-1(y, z)) → f.0-0(f.0-1(y, z), f.0-1(y, s.1(z)))
f.0-0(f.1-1(s.1(x), s.1(y)), f.0-1(z, w)) → f.0-0(f.1-1(x, y), f.0-1(z, w))
f.0-0(f.1-1(s.1(x), s.1(y)), f.0-0(z, w)) → f.0-0(f.1-1(x, y), f.0-0(z, w))
f.0-0(f.0-0(s.0(x), s.0(y)), f.1-1(z, w)) → f.0-0(f.0-0(x, y), f.1-1(z, w))
f.0-0(f.0-1(s.0(x), 0.), f.0-0(y, z)) → f.0-0(f.0-0(y, z), f.0-0(y, s.0(z)))
f.0-0(f.1-1(s.1(x), 0.), f.0-0(y, z)) → f.0-0(f.0-0(y, z), f.0-0(y, s.0(z)))
f.0-0(f.0-1(s.0(x), 0.), f.0-1(y, z)) → f.0-0(f.0-1(y, z), f.0-1(y, s.1(z)))
f.0-0(f.1-1(s.1(x), s.1(y)), f.1-1(z, w)) → f.0-0(f.1-1(x, y), f.1-1(z, w))
f.0-0(f.0-0(s.0(x), s.0(y)), f.0-0(z, w)) → f.0-0(f.0-0(x, y), f.0-0(z, w))
f.0-0(f.1-1(s.1(x), 0.), f.1-0(y, z)) → f.0-0(f.1-0(y, z), f.1-0(y, s.0(z)))
f.0-0(f.0-1(s.0(x), s.1(y)), f.0-0(z, w)) → f.0-0(f.0-1(x, y), f.0-0(z, w))
f.0-0(f.1-0(s.1(x), s.0(y)), f.1-0(z, w)) → f.0-0(f.1-0(x, y), f.1-0(z, w))
f.0-0(f.1-0(s.1(x), s.0(y)), f.0-1(z, w)) → f.0-0(f.1-0(x, y), f.0-1(z, w))
f.0-0(f.0-1(s.0(x), s.1(y)), f.1-0(z, w)) → f.0-0(f.0-1(x, y), f.1-0(z, w))
f.0-0(f.0-1(s.0(x), s.1(y)), f.1-1(z, w)) → f.0-0(f.0-1(x, y), f.1-1(z, w))
f.0-0(f.1-1(s.1(x), 0.), f.1-1(y, z)) → f.0-0(f.1-1(y, z), f.1-1(y, s.1(z)))
f.0-0(f.1-0(s.1(x), s.0(y)), f.0-0(z, w)) → f.0-0(f.1-0(x, y), f.0-0(z, w))
f.0-0(f.0-1(s.0(x), 0.), f.1-0(y, z)) → f.0-0(f.1-0(y, z), f.1-0(y, s.0(z)))
f.0-0(f.1-0(s.1(x), s.0(y)), f.1-1(z, w)) → f.0-0(f.1-0(x, y), f.1-1(z, w))
POL(F.0-0(x1, x2)) = x1 + x2
POL(f.1-0(x1, x2)) = x1 + x2
POL(f.1-1(x1, x2)) = x1 + x2
POL(s.0(x1)) = x1
POL(s.1(x1)) = x1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ SemLabProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesReductionPairsProof
↳ QDP
↳ RuleRemovalProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ SemLabProof2
F.0-0(f.1-0(s.1(s.1(y_0)), s.0(s.0(y_1))), f.1-1(x2, x3)) → F.0-0(f.1-0(s.1(y_0), s.0(y_1)), f.1-1(x2, x3))
F.0-0(f.1-0(s.1(s.1(y_0)), s.0(s.0(y_1))), f.1-1(x2, x3)) → F.0-0(f.1-0(s.1(y_0), s.0(y_1)), f.1-1(x2, x3))
POL(F.0-0(x1, x2)) = x1 + x2
POL(f.1-0(x1, x2)) = x1 + x2
POL(f.1-1(x1, x2)) = x1 + x2
POL(s.0(x1)) = 1 + x1
POL(s.1(x1)) = x1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ SemLabProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesReductionPairsProof
↳ QDP
↳ RuleRemovalProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ SemLabProof2
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ SemLabProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesReductionPairsProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ SemLabProof2
F.0-0(f.1-0(s.1(s.1(y_0)), s.0(s.0(y_1))), f.1-0(x2, x3)) → F.0-0(f.1-0(s.1(y_0), s.0(y_1)), f.1-0(x2, x3))
f.0-0(f.0-0(s.0(x), s.0(y)), f.1-0(z, w)) → f.0-0(f.0-0(x, y), f.1-0(z, w))
f.0-0(f.1-1(s.1(x), s.1(y)), f.1-0(z, w)) → f.0-0(f.1-1(x, y), f.1-0(z, w))
f.0-0(f.0-1(s.0(x), s.1(y)), f.0-1(z, w)) → f.0-0(f.0-1(x, y), f.0-1(z, w))
f.0-0(f.0-0(s.0(x), s.0(y)), f.0-1(z, w)) → f.0-0(f.0-0(x, y), f.0-1(z, w))
f.0-0(f.0-1(s.0(x), 0.), f.1-1(y, z)) → f.0-0(f.1-1(y, z), f.1-1(y, s.1(z)))
f.0-0(f.1-1(s.1(x), 0.), f.0-1(y, z)) → f.0-0(f.0-1(y, z), f.0-1(y, s.1(z)))
f.0-0(f.1-1(s.1(x), s.1(y)), f.0-1(z, w)) → f.0-0(f.1-1(x, y), f.0-1(z, w))
f.0-0(f.1-1(s.1(x), s.1(y)), f.0-0(z, w)) → f.0-0(f.1-1(x, y), f.0-0(z, w))
f.0-0(f.0-0(s.0(x), s.0(y)), f.1-1(z, w)) → f.0-0(f.0-0(x, y), f.1-1(z, w))
f.0-0(f.0-1(s.0(x), 0.), f.0-0(y, z)) → f.0-0(f.0-0(y, z), f.0-0(y, s.0(z)))
f.0-0(f.1-1(s.1(x), 0.), f.0-0(y, z)) → f.0-0(f.0-0(y, z), f.0-0(y, s.0(z)))
f.0-0(f.0-1(s.0(x), 0.), f.0-1(y, z)) → f.0-0(f.0-1(y, z), f.0-1(y, s.1(z)))
f.0-0(f.1-1(s.1(x), s.1(y)), f.1-1(z, w)) → f.0-0(f.1-1(x, y), f.1-1(z, w))
f.0-0(f.0-0(s.0(x), s.0(y)), f.0-0(z, w)) → f.0-0(f.0-0(x, y), f.0-0(z, w))
f.0-0(f.1-1(s.1(x), 0.), f.1-0(y, z)) → f.0-0(f.1-0(y, z), f.1-0(y, s.0(z)))
f.0-0(f.0-1(s.0(x), s.1(y)), f.0-0(z, w)) → f.0-0(f.0-1(x, y), f.0-0(z, w))
f.0-0(f.1-0(s.1(x), s.0(y)), f.1-0(z, w)) → f.0-0(f.1-0(x, y), f.1-0(z, w))
f.0-0(f.1-0(s.1(x), s.0(y)), f.0-1(z, w)) → f.0-0(f.1-0(x, y), f.0-1(z, w))
f.0-0(f.0-1(s.0(x), s.1(y)), f.1-0(z, w)) → f.0-0(f.0-1(x, y), f.1-0(z, w))
f.0-0(f.0-1(s.0(x), s.1(y)), f.1-1(z, w)) → f.0-0(f.0-1(x, y), f.1-1(z, w))
f.0-0(f.1-1(s.1(x), 0.), f.1-1(y, z)) → f.0-0(f.1-1(y, z), f.1-1(y, s.1(z)))
f.0-0(f.1-0(s.1(x), s.0(y)), f.0-0(z, w)) → f.0-0(f.1-0(x, y), f.0-0(z, w))
f.0-0(f.0-1(s.0(x), 0.), f.1-0(y, z)) → f.0-0(f.1-0(y, z), f.1-0(y, s.0(z)))
f.0-0(f.1-0(s.1(x), s.0(y)), f.1-1(z, w)) → f.0-0(f.1-0(x, y), f.1-1(z, w))
POL(F.0-0(x1, x2)) = x1 + x2
POL(f.1-0(x1, x2)) = x1 + x2
POL(s.0(x1)) = x1
POL(s.1(x1)) = x1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ SemLabProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesReductionPairsProof
↳ QDP
↳ RuleRemovalProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ SemLabProof2
F.0-0(f.1-0(s.1(s.1(y_0)), s.0(s.0(y_1))), f.1-0(x2, x3)) → F.0-0(f.1-0(s.1(y_0), s.0(y_1)), f.1-0(x2, x3))
F.0-0(f.1-0(s.1(s.1(y_0)), s.0(s.0(y_1))), f.1-0(x2, x3)) → F.0-0(f.1-0(s.1(y_0), s.0(y_1)), f.1-0(x2, x3))
POL(F.0-0(x1, x2)) = x1 + x2
POL(f.1-0(x1, x2)) = x1 + x2
POL(s.0(x1)) = 1 + x1
POL(s.1(x1)) = x1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ SemLabProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesReductionPairsProof
↳ QDP
↳ RuleRemovalProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ SemLabProof2
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ SemLabProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesReductionPairsProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ SemLabProof2
F.0-0(f.1-0(s.1(s.1(y_0)), s.0(s.0(y_1))), f.0-1(x2, x3)) → F.0-0(f.1-0(s.1(y_0), s.0(y_1)), f.0-1(x2, x3))
f.0-0(f.0-0(s.0(x), s.0(y)), f.1-0(z, w)) → f.0-0(f.0-0(x, y), f.1-0(z, w))
f.0-0(f.1-1(s.1(x), s.1(y)), f.1-0(z, w)) → f.0-0(f.1-1(x, y), f.1-0(z, w))
f.0-0(f.0-1(s.0(x), s.1(y)), f.0-1(z, w)) → f.0-0(f.0-1(x, y), f.0-1(z, w))
f.0-0(f.0-0(s.0(x), s.0(y)), f.0-1(z, w)) → f.0-0(f.0-0(x, y), f.0-1(z, w))
f.0-0(f.0-1(s.0(x), 0.), f.1-1(y, z)) → f.0-0(f.1-1(y, z), f.1-1(y, s.1(z)))
f.0-0(f.1-1(s.1(x), 0.), f.0-1(y, z)) → f.0-0(f.0-1(y, z), f.0-1(y, s.1(z)))
f.0-0(f.1-1(s.1(x), s.1(y)), f.0-1(z, w)) → f.0-0(f.1-1(x, y), f.0-1(z, w))
f.0-0(f.1-1(s.1(x), s.1(y)), f.0-0(z, w)) → f.0-0(f.1-1(x, y), f.0-0(z, w))
f.0-0(f.0-0(s.0(x), s.0(y)), f.1-1(z, w)) → f.0-0(f.0-0(x, y), f.1-1(z, w))
f.0-0(f.0-1(s.0(x), 0.), f.0-0(y, z)) → f.0-0(f.0-0(y, z), f.0-0(y, s.0(z)))
f.0-0(f.1-1(s.1(x), 0.), f.0-0(y, z)) → f.0-0(f.0-0(y, z), f.0-0(y, s.0(z)))
f.0-0(f.0-1(s.0(x), 0.), f.0-1(y, z)) → f.0-0(f.0-1(y, z), f.0-1(y, s.1(z)))
f.0-0(f.1-1(s.1(x), s.1(y)), f.1-1(z, w)) → f.0-0(f.1-1(x, y), f.1-1(z, w))
f.0-0(f.0-0(s.0(x), s.0(y)), f.0-0(z, w)) → f.0-0(f.0-0(x, y), f.0-0(z, w))
f.0-0(f.1-1(s.1(x), 0.), f.1-0(y, z)) → f.0-0(f.1-0(y, z), f.1-0(y, s.0(z)))
f.0-0(f.0-1(s.0(x), s.1(y)), f.0-0(z, w)) → f.0-0(f.0-1(x, y), f.0-0(z, w))
f.0-0(f.1-0(s.1(x), s.0(y)), f.1-0(z, w)) → f.0-0(f.1-0(x, y), f.1-0(z, w))
f.0-0(f.1-0(s.1(x), s.0(y)), f.0-1(z, w)) → f.0-0(f.1-0(x, y), f.0-1(z, w))
f.0-0(f.0-1(s.0(x), s.1(y)), f.1-0(z, w)) → f.0-0(f.0-1(x, y), f.1-0(z, w))
f.0-0(f.0-1(s.0(x), s.1(y)), f.1-1(z, w)) → f.0-0(f.0-1(x, y), f.1-1(z, w))
f.0-0(f.1-1(s.1(x), 0.), f.1-1(y, z)) → f.0-0(f.1-1(y, z), f.1-1(y, s.1(z)))
f.0-0(f.1-0(s.1(x), s.0(y)), f.0-0(z, w)) → f.0-0(f.1-0(x, y), f.0-0(z, w))
f.0-0(f.0-1(s.0(x), 0.), f.1-0(y, z)) → f.0-0(f.1-0(y, z), f.1-0(y, s.0(z)))
f.0-0(f.1-0(s.1(x), s.0(y)), f.1-1(z, w)) → f.0-0(f.1-0(x, y), f.1-1(z, w))
POL(F.0-0(x1, x2)) = x1 + x2
POL(f.0-1(x1, x2)) = x1 + x2
POL(f.1-0(x1, x2)) = x1 + x2
POL(s.0(x1)) = x1
POL(s.1(x1)) = x1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ SemLabProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesReductionPairsProof
↳ QDP
↳ RuleRemovalProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ SemLabProof2
F.0-0(f.1-0(s.1(s.1(y_0)), s.0(s.0(y_1))), f.0-1(x2, x3)) → F.0-0(f.1-0(s.1(y_0), s.0(y_1)), f.0-1(x2, x3))
F.0-0(f.1-0(s.1(s.1(y_0)), s.0(s.0(y_1))), f.0-1(x2, x3)) → F.0-0(f.1-0(s.1(y_0), s.0(y_1)), f.0-1(x2, x3))
POL(F.0-0(x1, x2)) = x1 + x2
POL(f.0-1(x1, x2)) = x1 + x2
POL(f.1-0(x1, x2)) = x1 + x2
POL(s.0(x1)) = 1 + x1
POL(s.1(x1)) = x1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ SemLabProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesReductionPairsProof
↳ QDP
↳ RuleRemovalProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ SemLabProof2
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ SemLabProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ SemLabProof2
F.0-0(f.1-0(s.1(s.1(y_0)), s.0(s.0(y_1))), f.0-0(x2, x3)) → F.0-0(f.1-0(s.1(y_0), s.0(y_1)), f.0-0(x2, x3))
f.0-0(f.0-0(s.0(x), s.0(y)), f.1-0(z, w)) → f.0-0(f.0-0(x, y), f.1-0(z, w))
f.0-0(f.1-1(s.1(x), s.1(y)), f.1-0(z, w)) → f.0-0(f.1-1(x, y), f.1-0(z, w))
f.0-0(f.0-1(s.0(x), s.1(y)), f.0-1(z, w)) → f.0-0(f.0-1(x, y), f.0-1(z, w))
f.0-0(f.0-0(s.0(x), s.0(y)), f.0-1(z, w)) → f.0-0(f.0-0(x, y), f.0-1(z, w))
f.0-0(f.0-1(s.0(x), 0.), f.1-1(y, z)) → f.0-0(f.1-1(y, z), f.1-1(y, s.1(z)))
f.0-0(f.1-1(s.1(x), 0.), f.0-1(y, z)) → f.0-0(f.0-1(y, z), f.0-1(y, s.1(z)))
f.0-0(f.1-1(s.1(x), s.1(y)), f.0-1(z, w)) → f.0-0(f.1-1(x, y), f.0-1(z, w))
f.0-0(f.1-1(s.1(x), s.1(y)), f.0-0(z, w)) → f.0-0(f.1-1(x, y), f.0-0(z, w))
f.0-0(f.0-0(s.0(x), s.0(y)), f.1-1(z, w)) → f.0-0(f.0-0(x, y), f.1-1(z, w))
f.0-0(f.0-1(s.0(x), 0.), f.0-0(y, z)) → f.0-0(f.0-0(y, z), f.0-0(y, s.0(z)))
f.0-0(f.1-1(s.1(x), 0.), f.0-0(y, z)) → f.0-0(f.0-0(y, z), f.0-0(y, s.0(z)))
f.0-0(f.0-1(s.0(x), 0.), f.0-1(y, z)) → f.0-0(f.0-1(y, z), f.0-1(y, s.1(z)))
f.0-0(f.1-1(s.1(x), s.1(y)), f.1-1(z, w)) → f.0-0(f.1-1(x, y), f.1-1(z, w))
f.0-0(f.0-0(s.0(x), s.0(y)), f.0-0(z, w)) → f.0-0(f.0-0(x, y), f.0-0(z, w))
f.0-0(f.1-1(s.1(x), 0.), f.1-0(y, z)) → f.0-0(f.1-0(y, z), f.1-0(y, s.0(z)))
f.0-0(f.0-1(s.0(x), s.1(y)), f.0-0(z, w)) → f.0-0(f.0-1(x, y), f.0-0(z, w))
f.0-0(f.1-0(s.1(x), s.0(y)), f.1-0(z, w)) → f.0-0(f.1-0(x, y), f.1-0(z, w))
f.0-0(f.1-0(s.1(x), s.0(y)), f.0-1(z, w)) → f.0-0(f.1-0(x, y), f.0-1(z, w))
f.0-0(f.0-1(s.0(x), s.1(y)), f.1-0(z, w)) → f.0-0(f.0-1(x, y), f.1-0(z, w))
f.0-0(f.0-1(s.0(x), s.1(y)), f.1-1(z, w)) → f.0-0(f.0-1(x, y), f.1-1(z, w))
f.0-0(f.1-1(s.1(x), 0.), f.1-1(y, z)) → f.0-0(f.1-1(y, z), f.1-1(y, s.1(z)))
f.0-0(f.1-0(s.1(x), s.0(y)), f.0-0(z, w)) → f.0-0(f.1-0(x, y), f.0-0(z, w))
f.0-0(f.0-1(s.0(x), 0.), f.1-0(y, z)) → f.0-0(f.1-0(y, z), f.1-0(y, s.0(z)))
f.0-0(f.1-0(s.1(x), s.0(y)), f.1-1(z, w)) → f.0-0(f.1-0(x, y), f.1-1(z, w))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
F.0-0(f.1-0(s.1(s.1(y_0)), s.0(s.0(y_1))), f.0-0(x2, x3)) → F.0-0(f.1-0(s.1(y_0), s.0(y_1)), f.0-0(x2, x3))
POL(0.) = 0
POL(F.0-0(x1, x2)) = x1
POL(f.0-0(x1, x2)) = 0
POL(f.0-1(x1, x2)) = 0
POL(f.1-0(x1, x2)) = x1 + x2
POL(f.1-1(x1, x2)) = 0
POL(s.0(x1)) = 1 + x1
POL(s.1(x1)) = 1 + x1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ SemLabProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ SemLabProof2
f.0-0(f.0-0(s.0(x), s.0(y)), f.1-0(z, w)) → f.0-0(f.0-0(x, y), f.1-0(z, w))
f.0-0(f.1-1(s.1(x), s.1(y)), f.1-0(z, w)) → f.0-0(f.1-1(x, y), f.1-0(z, w))
f.0-0(f.0-1(s.0(x), s.1(y)), f.0-1(z, w)) → f.0-0(f.0-1(x, y), f.0-1(z, w))
f.0-0(f.0-0(s.0(x), s.0(y)), f.0-1(z, w)) → f.0-0(f.0-0(x, y), f.0-1(z, w))
f.0-0(f.0-1(s.0(x), 0.), f.1-1(y, z)) → f.0-0(f.1-1(y, z), f.1-1(y, s.1(z)))
f.0-0(f.1-1(s.1(x), 0.), f.0-1(y, z)) → f.0-0(f.0-1(y, z), f.0-1(y, s.1(z)))
f.0-0(f.1-1(s.1(x), s.1(y)), f.0-1(z, w)) → f.0-0(f.1-1(x, y), f.0-1(z, w))
f.0-0(f.1-1(s.1(x), s.1(y)), f.0-0(z, w)) → f.0-0(f.1-1(x, y), f.0-0(z, w))
f.0-0(f.0-0(s.0(x), s.0(y)), f.1-1(z, w)) → f.0-0(f.0-0(x, y), f.1-1(z, w))
f.0-0(f.0-1(s.0(x), 0.), f.0-0(y, z)) → f.0-0(f.0-0(y, z), f.0-0(y, s.0(z)))
f.0-0(f.1-1(s.1(x), 0.), f.0-0(y, z)) → f.0-0(f.0-0(y, z), f.0-0(y, s.0(z)))
f.0-0(f.0-1(s.0(x), 0.), f.0-1(y, z)) → f.0-0(f.0-1(y, z), f.0-1(y, s.1(z)))
f.0-0(f.1-1(s.1(x), s.1(y)), f.1-1(z, w)) → f.0-0(f.1-1(x, y), f.1-1(z, w))
f.0-0(f.0-0(s.0(x), s.0(y)), f.0-0(z, w)) → f.0-0(f.0-0(x, y), f.0-0(z, w))
f.0-0(f.1-1(s.1(x), 0.), f.1-0(y, z)) → f.0-0(f.1-0(y, z), f.1-0(y, s.0(z)))
f.0-0(f.0-1(s.0(x), s.1(y)), f.0-0(z, w)) → f.0-0(f.0-1(x, y), f.0-0(z, w))
f.0-0(f.1-0(s.1(x), s.0(y)), f.1-0(z, w)) → f.0-0(f.1-0(x, y), f.1-0(z, w))
f.0-0(f.1-0(s.1(x), s.0(y)), f.0-1(z, w)) → f.0-0(f.1-0(x, y), f.0-1(z, w))
f.0-0(f.0-1(s.0(x), s.1(y)), f.1-0(z, w)) → f.0-0(f.0-1(x, y), f.1-0(z, w))
f.0-0(f.0-1(s.0(x), s.1(y)), f.1-1(z, w)) → f.0-0(f.0-1(x, y), f.1-1(z, w))
f.0-0(f.1-1(s.1(x), 0.), f.1-1(y, z)) → f.0-0(f.1-1(y, z), f.1-1(y, s.1(z)))
f.0-0(f.1-0(s.1(x), s.0(y)), f.0-0(z, w)) → f.0-0(f.1-0(x, y), f.0-0(z, w))
f.0-0(f.0-1(s.0(x), 0.), f.1-0(y, z)) → f.0-0(f.1-0(y, z), f.1-0(y, s.0(z)))
f.0-0(f.1-0(s.1(x), s.0(y)), f.1-1(z, w)) → f.0-0(f.1-0(x, y), f.1-1(z, w))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ SemLabProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesReductionPairsProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ SemLabProof2
F.0-0(f.1-1(s.1(s.1(y_0)), s.1(s.1(y_1))), f.1-0(x2, x3)) → F.0-0(f.1-1(s.1(y_0), s.1(y_1)), f.1-0(x2, x3))
f.0-0(f.0-0(s.0(x), s.0(y)), f.1-0(z, w)) → f.0-0(f.0-0(x, y), f.1-0(z, w))
f.0-0(f.1-1(s.1(x), s.1(y)), f.1-0(z, w)) → f.0-0(f.1-1(x, y), f.1-0(z, w))
f.0-0(f.0-1(s.0(x), s.1(y)), f.0-1(z, w)) → f.0-0(f.0-1(x, y), f.0-1(z, w))
f.0-0(f.0-0(s.0(x), s.0(y)), f.0-1(z, w)) → f.0-0(f.0-0(x, y), f.0-1(z, w))
f.0-0(f.0-1(s.0(x), 0.), f.1-1(y, z)) → f.0-0(f.1-1(y, z), f.1-1(y, s.1(z)))
f.0-0(f.1-1(s.1(x), 0.), f.0-1(y, z)) → f.0-0(f.0-1(y, z), f.0-1(y, s.1(z)))
f.0-0(f.1-1(s.1(x), s.1(y)), f.0-1(z, w)) → f.0-0(f.1-1(x, y), f.0-1(z, w))
f.0-0(f.1-1(s.1(x), s.1(y)), f.0-0(z, w)) → f.0-0(f.1-1(x, y), f.0-0(z, w))
f.0-0(f.0-0(s.0(x), s.0(y)), f.1-1(z, w)) → f.0-0(f.0-0(x, y), f.1-1(z, w))
f.0-0(f.0-1(s.0(x), 0.), f.0-0(y, z)) → f.0-0(f.0-0(y, z), f.0-0(y, s.0(z)))
f.0-0(f.1-1(s.1(x), 0.), f.0-0(y, z)) → f.0-0(f.0-0(y, z), f.0-0(y, s.0(z)))
f.0-0(f.0-1(s.0(x), 0.), f.0-1(y, z)) → f.0-0(f.0-1(y, z), f.0-1(y, s.1(z)))
f.0-0(f.1-1(s.1(x), s.1(y)), f.1-1(z, w)) → f.0-0(f.1-1(x, y), f.1-1(z, w))
f.0-0(f.0-0(s.0(x), s.0(y)), f.0-0(z, w)) → f.0-0(f.0-0(x, y), f.0-0(z, w))
f.0-0(f.1-1(s.1(x), 0.), f.1-0(y, z)) → f.0-0(f.1-0(y, z), f.1-0(y, s.0(z)))
f.0-0(f.0-1(s.0(x), s.1(y)), f.0-0(z, w)) → f.0-0(f.0-1(x, y), f.0-0(z, w))
f.0-0(f.1-0(s.1(x), s.0(y)), f.1-0(z, w)) → f.0-0(f.1-0(x, y), f.1-0(z, w))
f.0-0(f.1-0(s.1(x), s.0(y)), f.0-1(z, w)) → f.0-0(f.1-0(x, y), f.0-1(z, w))
f.0-0(f.0-1(s.0(x), s.1(y)), f.1-0(z, w)) → f.0-0(f.0-1(x, y), f.1-0(z, w))
f.0-0(f.0-1(s.0(x), s.1(y)), f.1-1(z, w)) → f.0-0(f.0-1(x, y), f.1-1(z, w))
f.0-0(f.1-1(s.1(x), 0.), f.1-1(y, z)) → f.0-0(f.1-1(y, z), f.1-1(y, s.1(z)))
f.0-0(f.1-0(s.1(x), s.0(y)), f.0-0(z, w)) → f.0-0(f.1-0(x, y), f.0-0(z, w))
f.0-0(f.0-1(s.0(x), 0.), f.1-0(y, z)) → f.0-0(f.1-0(y, z), f.1-0(y, s.0(z)))
f.0-0(f.1-0(s.1(x), s.0(y)), f.1-1(z, w)) → f.0-0(f.1-0(x, y), f.1-1(z, w))
POL(F.0-0(x1, x2)) = x1 + x2
POL(f.1-0(x1, x2)) = x1 + x2
POL(f.1-1(x1, x2)) = x1 + x2
POL(s.1(x1)) = x1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ SemLabProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesReductionPairsProof
↳ QDP
↳ RuleRemovalProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ SemLabProof2
F.0-0(f.1-1(s.1(s.1(y_0)), s.1(s.1(y_1))), f.1-0(x2, x3)) → F.0-0(f.1-1(s.1(y_0), s.1(y_1)), f.1-0(x2, x3))
F.0-0(f.1-1(s.1(s.1(y_0)), s.1(s.1(y_1))), f.1-0(x2, x3)) → F.0-0(f.1-1(s.1(y_0), s.1(y_1)), f.1-0(x2, x3))
POL(F.0-0(x1, x2)) = x1 + x2
POL(f.1-0(x1, x2)) = x1 + x2
POL(f.1-1(x1, x2)) = x1 + x2
POL(s.1(x1)) = 1 + x1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ SemLabProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesReductionPairsProof
↳ QDP
↳ RuleRemovalProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ SemLabProof2
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ SemLabProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesReductionPairsProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ SemLabProof2
F.0-0(f.0-1(s.0(s.0(y_0)), s.1(s.1(y_1))), f.1-0(x2, x3)) → F.0-0(f.0-1(s.0(y_0), s.1(y_1)), f.1-0(x2, x3))
f.0-0(f.0-0(s.0(x), s.0(y)), f.1-0(z, w)) → f.0-0(f.0-0(x, y), f.1-0(z, w))
f.0-0(f.1-1(s.1(x), s.1(y)), f.1-0(z, w)) → f.0-0(f.1-1(x, y), f.1-0(z, w))
f.0-0(f.0-1(s.0(x), s.1(y)), f.0-1(z, w)) → f.0-0(f.0-1(x, y), f.0-1(z, w))
f.0-0(f.0-0(s.0(x), s.0(y)), f.0-1(z, w)) → f.0-0(f.0-0(x, y), f.0-1(z, w))
f.0-0(f.0-1(s.0(x), 0.), f.1-1(y, z)) → f.0-0(f.1-1(y, z), f.1-1(y, s.1(z)))
f.0-0(f.1-1(s.1(x), 0.), f.0-1(y, z)) → f.0-0(f.0-1(y, z), f.0-1(y, s.1(z)))
f.0-0(f.1-1(s.1(x), s.1(y)), f.0-1(z, w)) → f.0-0(f.1-1(x, y), f.0-1(z, w))
f.0-0(f.1-1(s.1(x), s.1(y)), f.0-0(z, w)) → f.0-0(f.1-1(x, y), f.0-0(z, w))
f.0-0(f.0-0(s.0(x), s.0(y)), f.1-1(z, w)) → f.0-0(f.0-0(x, y), f.1-1(z, w))
f.0-0(f.0-1(s.0(x), 0.), f.0-0(y, z)) → f.0-0(f.0-0(y, z), f.0-0(y, s.0(z)))
f.0-0(f.1-1(s.1(x), 0.), f.0-0(y, z)) → f.0-0(f.0-0(y, z), f.0-0(y, s.0(z)))
f.0-0(f.0-1(s.0(x), 0.), f.0-1(y, z)) → f.0-0(f.0-1(y, z), f.0-1(y, s.1(z)))
f.0-0(f.1-1(s.1(x), s.1(y)), f.1-1(z, w)) → f.0-0(f.1-1(x, y), f.1-1(z, w))
f.0-0(f.0-0(s.0(x), s.0(y)), f.0-0(z, w)) → f.0-0(f.0-0(x, y), f.0-0(z, w))
f.0-0(f.1-1(s.1(x), 0.), f.1-0(y, z)) → f.0-0(f.1-0(y, z), f.1-0(y, s.0(z)))
f.0-0(f.0-1(s.0(x), s.1(y)), f.0-0(z, w)) → f.0-0(f.0-1(x, y), f.0-0(z, w))
f.0-0(f.1-0(s.1(x), s.0(y)), f.1-0(z, w)) → f.0-0(f.1-0(x, y), f.1-0(z, w))
f.0-0(f.1-0(s.1(x), s.0(y)), f.0-1(z, w)) → f.0-0(f.1-0(x, y), f.0-1(z, w))
f.0-0(f.0-1(s.0(x), s.1(y)), f.1-0(z, w)) → f.0-0(f.0-1(x, y), f.1-0(z, w))
f.0-0(f.0-1(s.0(x), s.1(y)), f.1-1(z, w)) → f.0-0(f.0-1(x, y), f.1-1(z, w))
f.0-0(f.1-1(s.1(x), 0.), f.1-1(y, z)) → f.0-0(f.1-1(y, z), f.1-1(y, s.1(z)))
f.0-0(f.1-0(s.1(x), s.0(y)), f.0-0(z, w)) → f.0-0(f.1-0(x, y), f.0-0(z, w))
f.0-0(f.0-1(s.0(x), 0.), f.1-0(y, z)) → f.0-0(f.1-0(y, z), f.1-0(y, s.0(z)))
f.0-0(f.1-0(s.1(x), s.0(y)), f.1-1(z, w)) → f.0-0(f.1-0(x, y), f.1-1(z, w))
POL(F.0-0(x1, x2)) = x1 + x2
POL(f.0-1(x1, x2)) = x1 + x2
POL(f.1-0(x1, x2)) = x1 + x2
POL(s.0(x1)) = x1
POL(s.1(x1)) = x1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ SemLabProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesReductionPairsProof
↳ QDP
↳ RuleRemovalProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ SemLabProof2
F.0-0(f.0-1(s.0(s.0(y_0)), s.1(s.1(y_1))), f.1-0(x2, x3)) → F.0-0(f.0-1(s.0(y_0), s.1(y_1)), f.1-0(x2, x3))
F.0-0(f.0-1(s.0(s.0(y_0)), s.1(s.1(y_1))), f.1-0(x2, x3)) → F.0-0(f.0-1(s.0(y_0), s.1(y_1)), f.1-0(x2, x3))
POL(F.0-0(x1, x2)) = x1 + x2
POL(f.0-1(x1, x2)) = x1 + x2
POL(f.1-0(x1, x2)) = x1 + x2
POL(s.0(x1)) = x1
POL(s.1(x1)) = 1 + x1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ SemLabProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesReductionPairsProof
↳ QDP
↳ RuleRemovalProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ SemLabProof2
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ SemLabProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ SemLabProof2
F.0-0(f.1-1(s.1(s.1(y_0)), s.1(0.)), f.1-1(x2, x3)) → F.0-0(f.1-1(s.1(y_0), 0.), f.1-1(x2, x3))
F.0-0(f.1-1(s.1(x0), 0.), f.1-1(s.1(s.1(y_0)), s.1(0.))) → F.0-0(f.1-1(s.1(s.1(y_0)), s.1(0.)), f.1-1(s.1(s.1(y_0)), s.1(s.1(0.))))
F.0-0(f.1-1(s.1(x0), 0.), f.1-1(s.1(y_0), 0.)) → F.0-0(f.1-1(s.1(y_0), 0.), f.1-1(s.1(y_0), s.1(0.)))
F.0-0(f.1-1(s.1(s.1(y_0)), s.1(s.1(y_1))), f.1-1(x2, x3)) → F.0-0(f.1-1(s.1(y_0), s.1(y_1)), f.1-1(x2, x3))
F.0-0(f.1-1(s.1(x0), 0.), f.1-1(s.1(y_0), s.1(y_1))) → F.0-0(f.1-1(s.1(y_0), s.1(y_1)), f.1-1(s.1(y_0), s.1(s.1(y_1))))
F.0-0(f.1-1(s.1(x0), 0.), f.1-1(s.1(s.1(y_0)), s.1(s.1(y_1)))) → F.0-0(f.1-1(s.1(s.1(y_0)), s.1(s.1(y_1))), f.1-1(s.1(s.1(y_0)), s.1(s.1(s.1(y_1)))))
f.0-0(f.0-0(s.0(x), s.0(y)), f.1-0(z, w)) → f.0-0(f.0-0(x, y), f.1-0(z, w))
f.0-0(f.1-1(s.1(x), s.1(y)), f.1-0(z, w)) → f.0-0(f.1-1(x, y), f.1-0(z, w))
f.0-0(f.0-1(s.0(x), s.1(y)), f.0-1(z, w)) → f.0-0(f.0-1(x, y), f.0-1(z, w))
f.0-0(f.0-0(s.0(x), s.0(y)), f.0-1(z, w)) → f.0-0(f.0-0(x, y), f.0-1(z, w))
f.0-0(f.0-1(s.0(x), 0.), f.1-1(y, z)) → f.0-0(f.1-1(y, z), f.1-1(y, s.1(z)))
f.0-0(f.1-1(s.1(x), 0.), f.0-1(y, z)) → f.0-0(f.0-1(y, z), f.0-1(y, s.1(z)))
f.0-0(f.1-1(s.1(x), s.1(y)), f.0-1(z, w)) → f.0-0(f.1-1(x, y), f.0-1(z, w))
f.0-0(f.1-1(s.1(x), s.1(y)), f.0-0(z, w)) → f.0-0(f.1-1(x, y), f.0-0(z, w))
f.0-0(f.0-0(s.0(x), s.0(y)), f.1-1(z, w)) → f.0-0(f.0-0(x, y), f.1-1(z, w))
f.0-0(f.0-1(s.0(x), 0.), f.0-0(y, z)) → f.0-0(f.0-0(y, z), f.0-0(y, s.0(z)))
f.0-0(f.1-1(s.1(x), 0.), f.0-0(y, z)) → f.0-0(f.0-0(y, z), f.0-0(y, s.0(z)))
f.0-0(f.0-1(s.0(x), 0.), f.0-1(y, z)) → f.0-0(f.0-1(y, z), f.0-1(y, s.1(z)))
f.0-0(f.1-1(s.1(x), s.1(y)), f.1-1(z, w)) → f.0-0(f.1-1(x, y), f.1-1(z, w))
f.0-0(f.0-0(s.0(x), s.0(y)), f.0-0(z, w)) → f.0-0(f.0-0(x, y), f.0-0(z, w))
f.0-0(f.1-1(s.1(x), 0.), f.1-0(y, z)) → f.0-0(f.1-0(y, z), f.1-0(y, s.0(z)))
f.0-0(f.0-1(s.0(x), s.1(y)), f.0-0(z, w)) → f.0-0(f.0-1(x, y), f.0-0(z, w))
f.0-0(f.1-0(s.1(x), s.0(y)), f.1-0(z, w)) → f.0-0(f.1-0(x, y), f.1-0(z, w))
f.0-0(f.1-0(s.1(x), s.0(y)), f.0-1(z, w)) → f.0-0(f.1-0(x, y), f.0-1(z, w))
f.0-0(f.0-1(s.0(x), s.1(y)), f.1-0(z, w)) → f.0-0(f.0-1(x, y), f.1-0(z, w))
f.0-0(f.0-1(s.0(x), s.1(y)), f.1-1(z, w)) → f.0-0(f.0-1(x, y), f.1-1(z, w))
f.0-0(f.1-1(s.1(x), 0.), f.1-1(y, z)) → f.0-0(f.1-1(y, z), f.1-1(y, s.1(z)))
f.0-0(f.1-0(s.1(x), s.0(y)), f.0-0(z, w)) → f.0-0(f.1-0(x, y), f.0-0(z, w))
f.0-0(f.0-1(s.0(x), 0.), f.1-0(y, z)) → f.0-0(f.1-0(y, z), f.1-0(y, s.0(z)))
f.0-0(f.1-0(s.1(x), s.0(y)), f.1-1(z, w)) → f.0-0(f.1-0(x, y), f.1-1(z, w))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
F.0-0(f.1-1(s.1(x0), 0.), f.1-1(s.1(y_0), 0.)) → F.0-0(f.1-1(s.1(y_0), 0.), f.1-1(s.1(y_0), s.1(0.)))
Used ordering: Polynomial interpretation [25]:
F.0-0(f.1-1(s.1(s.1(y_0)), s.1(0.)), f.1-1(x2, x3)) → F.0-0(f.1-1(s.1(y_0), 0.), f.1-1(x2, x3))
F.0-0(f.1-1(s.1(x0), 0.), f.1-1(s.1(s.1(y_0)), s.1(0.))) → F.0-0(f.1-1(s.1(s.1(y_0)), s.1(0.)), f.1-1(s.1(s.1(y_0)), s.1(s.1(0.))))
F.0-0(f.1-1(s.1(s.1(y_0)), s.1(s.1(y_1))), f.1-1(x2, x3)) → F.0-0(f.1-1(s.1(y_0), s.1(y_1)), f.1-1(x2, x3))
F.0-0(f.1-1(s.1(x0), 0.), f.1-1(s.1(y_0), s.1(y_1))) → F.0-0(f.1-1(s.1(y_0), s.1(y_1)), f.1-1(s.1(y_0), s.1(s.1(y_1))))
F.0-0(f.1-1(s.1(x0), 0.), f.1-1(s.1(s.1(y_0)), s.1(s.1(y_1)))) → F.0-0(f.1-1(s.1(s.1(y_0)), s.1(s.1(y_1))), f.1-1(s.1(s.1(y_0)), s.1(s.1(s.1(y_1)))))
POL(0.) = 1
POL(F.0-0(x1, x2)) = x2
POL(f.1-1(x1, x2)) = x2
POL(s.1(x1)) = 0
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ SemLabProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ SemLabProof2
F.0-0(f.1-1(s.1(s.1(y_0)), s.1(0.)), f.1-1(x2, x3)) → F.0-0(f.1-1(s.1(y_0), 0.), f.1-1(x2, x3))
F.0-0(f.1-1(s.1(x0), 0.), f.1-1(s.1(s.1(y_0)), s.1(0.))) → F.0-0(f.1-1(s.1(s.1(y_0)), s.1(0.)), f.1-1(s.1(s.1(y_0)), s.1(s.1(0.))))
F.0-0(f.1-1(s.1(x0), 0.), f.1-1(s.1(y_0), s.1(y_1))) → F.0-0(f.1-1(s.1(y_0), s.1(y_1)), f.1-1(s.1(y_0), s.1(s.1(y_1))))
F.0-0(f.1-1(s.1(s.1(y_0)), s.1(s.1(y_1))), f.1-1(x2, x3)) → F.0-0(f.1-1(s.1(y_0), s.1(y_1)), f.1-1(x2, x3))
F.0-0(f.1-1(s.1(x0), 0.), f.1-1(s.1(s.1(y_0)), s.1(s.1(y_1)))) → F.0-0(f.1-1(s.1(s.1(y_0)), s.1(s.1(y_1))), f.1-1(s.1(s.1(y_0)), s.1(s.1(s.1(y_1)))))
f.0-0(f.0-0(s.0(x), s.0(y)), f.1-0(z, w)) → f.0-0(f.0-0(x, y), f.1-0(z, w))
f.0-0(f.1-1(s.1(x), s.1(y)), f.1-0(z, w)) → f.0-0(f.1-1(x, y), f.1-0(z, w))
f.0-0(f.0-1(s.0(x), s.1(y)), f.0-1(z, w)) → f.0-0(f.0-1(x, y), f.0-1(z, w))
f.0-0(f.0-0(s.0(x), s.0(y)), f.0-1(z, w)) → f.0-0(f.0-0(x, y), f.0-1(z, w))
f.0-0(f.0-1(s.0(x), 0.), f.1-1(y, z)) → f.0-0(f.1-1(y, z), f.1-1(y, s.1(z)))
f.0-0(f.1-1(s.1(x), 0.), f.0-1(y, z)) → f.0-0(f.0-1(y, z), f.0-1(y, s.1(z)))
f.0-0(f.1-1(s.1(x), s.1(y)), f.0-1(z, w)) → f.0-0(f.1-1(x, y), f.0-1(z, w))
f.0-0(f.1-1(s.1(x), s.1(y)), f.0-0(z, w)) → f.0-0(f.1-1(x, y), f.0-0(z, w))
f.0-0(f.0-0(s.0(x), s.0(y)), f.1-1(z, w)) → f.0-0(f.0-0(x, y), f.1-1(z, w))
f.0-0(f.0-1(s.0(x), 0.), f.0-0(y, z)) → f.0-0(f.0-0(y, z), f.0-0(y, s.0(z)))
f.0-0(f.1-1(s.1(x), 0.), f.0-0(y, z)) → f.0-0(f.0-0(y, z), f.0-0(y, s.0(z)))
f.0-0(f.0-1(s.0(x), 0.), f.0-1(y, z)) → f.0-0(f.0-1(y, z), f.0-1(y, s.1(z)))
f.0-0(f.1-1(s.1(x), s.1(y)), f.1-1(z, w)) → f.0-0(f.1-1(x, y), f.1-1(z, w))
f.0-0(f.0-0(s.0(x), s.0(y)), f.0-0(z, w)) → f.0-0(f.0-0(x, y), f.0-0(z, w))
f.0-0(f.1-1(s.1(x), 0.), f.1-0(y, z)) → f.0-0(f.1-0(y, z), f.1-0(y, s.0(z)))
f.0-0(f.0-1(s.0(x), s.1(y)), f.0-0(z, w)) → f.0-0(f.0-1(x, y), f.0-0(z, w))
f.0-0(f.1-0(s.1(x), s.0(y)), f.1-0(z, w)) → f.0-0(f.1-0(x, y), f.1-0(z, w))
f.0-0(f.1-0(s.1(x), s.0(y)), f.0-1(z, w)) → f.0-0(f.1-0(x, y), f.0-1(z, w))
f.0-0(f.0-1(s.0(x), s.1(y)), f.1-0(z, w)) → f.0-0(f.0-1(x, y), f.1-0(z, w))
f.0-0(f.0-1(s.0(x), s.1(y)), f.1-1(z, w)) → f.0-0(f.0-1(x, y), f.1-1(z, w))
f.0-0(f.1-1(s.1(x), 0.), f.1-1(y, z)) → f.0-0(f.1-1(y, z), f.1-1(y, s.1(z)))
f.0-0(f.1-0(s.1(x), s.0(y)), f.0-0(z, w)) → f.0-0(f.1-0(x, y), f.0-0(z, w))
f.0-0(f.0-1(s.0(x), 0.), f.1-0(y, z)) → f.0-0(f.1-0(y, z), f.1-0(y, s.0(z)))
f.0-0(f.1-0(s.1(x), s.0(y)), f.1-1(z, w)) → f.0-0(f.1-0(x, y), f.1-1(z, w))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ SemLabProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesReductionPairsProof
↳ QDP
↳ QDP
↳ QDP
↳ SemLabProof2
F.0-0(f.0-1(s.0(s.0(y_0)), s.1(s.1(y_1))), f.1-1(x2, x3)) → F.0-0(f.0-1(s.0(y_0), s.1(y_1)), f.1-1(x2, x3))
f.0-0(f.0-0(s.0(x), s.0(y)), f.1-0(z, w)) → f.0-0(f.0-0(x, y), f.1-0(z, w))
f.0-0(f.1-1(s.1(x), s.1(y)), f.1-0(z, w)) → f.0-0(f.1-1(x, y), f.1-0(z, w))
f.0-0(f.0-1(s.0(x), s.1(y)), f.0-1(z, w)) → f.0-0(f.0-1(x, y), f.0-1(z, w))
f.0-0(f.0-0(s.0(x), s.0(y)), f.0-1(z, w)) → f.0-0(f.0-0(x, y), f.0-1(z, w))
f.0-0(f.0-1(s.0(x), 0.), f.1-1(y, z)) → f.0-0(f.1-1(y, z), f.1-1(y, s.1(z)))
f.0-0(f.1-1(s.1(x), 0.), f.0-1(y, z)) → f.0-0(f.0-1(y, z), f.0-1(y, s.1(z)))
f.0-0(f.1-1(s.1(x), s.1(y)), f.0-1(z, w)) → f.0-0(f.1-1(x, y), f.0-1(z, w))
f.0-0(f.1-1(s.1(x), s.1(y)), f.0-0(z, w)) → f.0-0(f.1-1(x, y), f.0-0(z, w))
f.0-0(f.0-0(s.0(x), s.0(y)), f.1-1(z, w)) → f.0-0(f.0-0(x, y), f.1-1(z, w))
f.0-0(f.0-1(s.0(x), 0.), f.0-0(y, z)) → f.0-0(f.0-0(y, z), f.0-0(y, s.0(z)))
f.0-0(f.1-1(s.1(x), 0.), f.0-0(y, z)) → f.0-0(f.0-0(y, z), f.0-0(y, s.0(z)))
f.0-0(f.0-1(s.0(x), 0.), f.0-1(y, z)) → f.0-0(f.0-1(y, z), f.0-1(y, s.1(z)))
f.0-0(f.1-1(s.1(x), s.1(y)), f.1-1(z, w)) → f.0-0(f.1-1(x, y), f.1-1(z, w))
f.0-0(f.0-0(s.0(x), s.0(y)), f.0-0(z, w)) → f.0-0(f.0-0(x, y), f.0-0(z, w))
f.0-0(f.1-1(s.1(x), 0.), f.1-0(y, z)) → f.0-0(f.1-0(y, z), f.1-0(y, s.0(z)))
f.0-0(f.0-1(s.0(x), s.1(y)), f.0-0(z, w)) → f.0-0(f.0-1(x, y), f.0-0(z, w))
f.0-0(f.1-0(s.1(x), s.0(y)), f.1-0(z, w)) → f.0-0(f.1-0(x, y), f.1-0(z, w))
f.0-0(f.1-0(s.1(x), s.0(y)), f.0-1(z, w)) → f.0-0(f.1-0(x, y), f.0-1(z, w))
f.0-0(f.0-1(s.0(x), s.1(y)), f.1-0(z, w)) → f.0-0(f.0-1(x, y), f.1-0(z, w))
f.0-0(f.0-1(s.0(x), s.1(y)), f.1-1(z, w)) → f.0-0(f.0-1(x, y), f.1-1(z, w))
f.0-0(f.1-1(s.1(x), 0.), f.1-1(y, z)) → f.0-0(f.1-1(y, z), f.1-1(y, s.1(z)))
f.0-0(f.1-0(s.1(x), s.0(y)), f.0-0(z, w)) → f.0-0(f.1-0(x, y), f.0-0(z, w))
f.0-0(f.0-1(s.0(x), 0.), f.1-0(y, z)) → f.0-0(f.1-0(y, z), f.1-0(y, s.0(z)))
f.0-0(f.1-0(s.1(x), s.0(y)), f.1-1(z, w)) → f.0-0(f.1-0(x, y), f.1-1(z, w))
POL(F.0-0(x1, x2)) = x1 + x2
POL(f.0-1(x1, x2)) = x1 + x2
POL(f.1-1(x1, x2)) = x1 + x2
POL(s.0(x1)) = x1
POL(s.1(x1)) = x1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ SemLabProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesReductionPairsProof
↳ QDP
↳ RuleRemovalProof
↳ QDP
↳ QDP
↳ QDP
↳ SemLabProof2
F.0-0(f.0-1(s.0(s.0(y_0)), s.1(s.1(y_1))), f.1-1(x2, x3)) → F.0-0(f.0-1(s.0(y_0), s.1(y_1)), f.1-1(x2, x3))
F.0-0(f.0-1(s.0(s.0(y_0)), s.1(s.1(y_1))), f.1-1(x2, x3)) → F.0-0(f.0-1(s.0(y_0), s.1(y_1)), f.1-1(x2, x3))
POL(F.0-0(x1, x2)) = x1 + x2
POL(f.0-1(x1, x2)) = x1 + x2
POL(f.1-1(x1, x2)) = x1 + x2
POL(s.0(x1)) = x1
POL(s.1(x1)) = 1 + x1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ SemLabProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesReductionPairsProof
↳ QDP
↳ RuleRemovalProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
↳ QDP
↳ SemLabProof2
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ SemLabProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
↳ SemLabProof2
F.0-0(f.0-1(s.0(x0), 0.), f.0-1(s.0(s.0(y_0)), s.1(0.))) → F.0-0(f.0-1(s.0(s.0(y_0)), s.1(0.)), f.0-1(s.0(s.0(y_0)), s.1(s.1(0.))))
F.0-0(f.0-1(s.0(x0), 0.), f.0-1(s.0(y_0), 0.)) → F.0-0(f.0-1(s.0(y_0), 0.), f.0-1(s.0(y_0), s.1(0.)))
F.0-0(f.0-1(s.0(x0), 0.), f.0-1(s.0(y_0), s.1(y_1))) → F.0-0(f.0-1(s.0(y_0), s.1(y_1)), f.0-1(s.0(y_0), s.1(s.1(y_1))))
F.0-0(f.0-1(s.0(s.0(y_0)), s.1(s.1(y_1))), f.0-1(x2, x3)) → F.0-0(f.0-1(s.0(y_0), s.1(y_1)), f.0-1(x2, x3))
F.0-0(f.0-1(s.0(s.0(y_0)), s.1(0.)), f.0-1(x2, x3)) → F.0-0(f.0-1(s.0(y_0), 0.), f.0-1(x2, x3))
F.0-0(f.0-1(s.0(x0), 0.), f.0-1(s.0(s.0(y_0)), s.1(s.1(y_1)))) → F.0-0(f.0-1(s.0(s.0(y_0)), s.1(s.1(y_1))), f.0-1(s.0(s.0(y_0)), s.1(s.1(s.1(y_1)))))
f.0-0(f.0-0(s.0(x), s.0(y)), f.1-0(z, w)) → f.0-0(f.0-0(x, y), f.1-0(z, w))
f.0-0(f.1-1(s.1(x), s.1(y)), f.1-0(z, w)) → f.0-0(f.1-1(x, y), f.1-0(z, w))
f.0-0(f.0-1(s.0(x), s.1(y)), f.0-1(z, w)) → f.0-0(f.0-1(x, y), f.0-1(z, w))
f.0-0(f.0-0(s.0(x), s.0(y)), f.0-1(z, w)) → f.0-0(f.0-0(x, y), f.0-1(z, w))
f.0-0(f.0-1(s.0(x), 0.), f.1-1(y, z)) → f.0-0(f.1-1(y, z), f.1-1(y, s.1(z)))
f.0-0(f.1-1(s.1(x), 0.), f.0-1(y, z)) → f.0-0(f.0-1(y, z), f.0-1(y, s.1(z)))
f.0-0(f.1-1(s.1(x), s.1(y)), f.0-1(z, w)) → f.0-0(f.1-1(x, y), f.0-1(z, w))
f.0-0(f.1-1(s.1(x), s.1(y)), f.0-0(z, w)) → f.0-0(f.1-1(x, y), f.0-0(z, w))
f.0-0(f.0-0(s.0(x), s.0(y)), f.1-1(z, w)) → f.0-0(f.0-0(x, y), f.1-1(z, w))
f.0-0(f.0-1(s.0(x), 0.), f.0-0(y, z)) → f.0-0(f.0-0(y, z), f.0-0(y, s.0(z)))
f.0-0(f.1-1(s.1(x), 0.), f.0-0(y, z)) → f.0-0(f.0-0(y, z), f.0-0(y, s.0(z)))
f.0-0(f.0-1(s.0(x), 0.), f.0-1(y, z)) → f.0-0(f.0-1(y, z), f.0-1(y, s.1(z)))
f.0-0(f.1-1(s.1(x), s.1(y)), f.1-1(z, w)) → f.0-0(f.1-1(x, y), f.1-1(z, w))
f.0-0(f.0-0(s.0(x), s.0(y)), f.0-0(z, w)) → f.0-0(f.0-0(x, y), f.0-0(z, w))
f.0-0(f.1-1(s.1(x), 0.), f.1-0(y, z)) → f.0-0(f.1-0(y, z), f.1-0(y, s.0(z)))
f.0-0(f.0-1(s.0(x), s.1(y)), f.0-0(z, w)) → f.0-0(f.0-1(x, y), f.0-0(z, w))
f.0-0(f.1-0(s.1(x), s.0(y)), f.1-0(z, w)) → f.0-0(f.1-0(x, y), f.1-0(z, w))
f.0-0(f.1-0(s.1(x), s.0(y)), f.0-1(z, w)) → f.0-0(f.1-0(x, y), f.0-1(z, w))
f.0-0(f.0-1(s.0(x), s.1(y)), f.1-0(z, w)) → f.0-0(f.0-1(x, y), f.1-0(z, w))
f.0-0(f.0-1(s.0(x), s.1(y)), f.1-1(z, w)) → f.0-0(f.0-1(x, y), f.1-1(z, w))
f.0-0(f.1-1(s.1(x), 0.), f.1-1(y, z)) → f.0-0(f.1-1(y, z), f.1-1(y, s.1(z)))
f.0-0(f.1-0(s.1(x), s.0(y)), f.0-0(z, w)) → f.0-0(f.1-0(x, y), f.0-0(z, w))
f.0-0(f.0-1(s.0(x), 0.), f.1-0(y, z)) → f.0-0(f.1-0(y, z), f.1-0(y, s.0(z)))
f.0-0(f.1-0(s.1(x), s.0(y)), f.1-1(z, w)) → f.0-0(f.1-0(x, y), f.1-1(z, w))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
F.0-0(f.0-1(s.0(x0), 0.), f.0-1(s.0(y_0), 0.)) → F.0-0(f.0-1(s.0(y_0), 0.), f.0-1(s.0(y_0), s.1(0.)))
Used ordering: Polynomial interpretation [25]:
F.0-0(f.0-1(s.0(x0), 0.), f.0-1(s.0(s.0(y_0)), s.1(0.))) → F.0-0(f.0-1(s.0(s.0(y_0)), s.1(0.)), f.0-1(s.0(s.0(y_0)), s.1(s.1(0.))))
F.0-0(f.0-1(s.0(x0), 0.), f.0-1(s.0(y_0), s.1(y_1))) → F.0-0(f.0-1(s.0(y_0), s.1(y_1)), f.0-1(s.0(y_0), s.1(s.1(y_1))))
F.0-0(f.0-1(s.0(s.0(y_0)), s.1(s.1(y_1))), f.0-1(x2, x3)) → F.0-0(f.0-1(s.0(y_0), s.1(y_1)), f.0-1(x2, x3))
F.0-0(f.0-1(s.0(s.0(y_0)), s.1(0.)), f.0-1(x2, x3)) → F.0-0(f.0-1(s.0(y_0), 0.), f.0-1(x2, x3))
F.0-0(f.0-1(s.0(x0), 0.), f.0-1(s.0(s.0(y_0)), s.1(s.1(y_1)))) → F.0-0(f.0-1(s.0(s.0(y_0)), s.1(s.1(y_1))), f.0-1(s.0(s.0(y_0)), s.1(s.1(s.1(y_1)))))
POL(0.) = 1
POL(F.0-0(x1, x2)) = x2
POL(f.0-1(x1, x2)) = x2
POL(s.0(x1)) = 0
POL(s.1(x1)) = 0
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ SemLabProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
↳ QDP
↳ SemLabProof2
F.0-0(f.0-1(s.0(x0), 0.), f.0-1(s.0(s.0(y_0)), s.1(0.))) → F.0-0(f.0-1(s.0(s.0(y_0)), s.1(0.)), f.0-1(s.0(s.0(y_0)), s.1(s.1(0.))))
F.0-0(f.0-1(s.0(x0), 0.), f.0-1(s.0(y_0), s.1(y_1))) → F.0-0(f.0-1(s.0(y_0), s.1(y_1)), f.0-1(s.0(y_0), s.1(s.1(y_1))))
F.0-0(f.0-1(s.0(s.0(y_0)), s.1(0.)), f.0-1(x2, x3)) → F.0-0(f.0-1(s.0(y_0), 0.), f.0-1(x2, x3))
F.0-0(f.0-1(s.0(s.0(y_0)), s.1(s.1(y_1))), f.0-1(x2, x3)) → F.0-0(f.0-1(s.0(y_0), s.1(y_1)), f.0-1(x2, x3))
F.0-0(f.0-1(s.0(x0), 0.), f.0-1(s.0(s.0(y_0)), s.1(s.1(y_1)))) → F.0-0(f.0-1(s.0(s.0(y_0)), s.1(s.1(y_1))), f.0-1(s.0(s.0(y_0)), s.1(s.1(s.1(y_1)))))
f.0-0(f.0-0(s.0(x), s.0(y)), f.1-0(z, w)) → f.0-0(f.0-0(x, y), f.1-0(z, w))
f.0-0(f.1-1(s.1(x), s.1(y)), f.1-0(z, w)) → f.0-0(f.1-1(x, y), f.1-0(z, w))
f.0-0(f.0-1(s.0(x), s.1(y)), f.0-1(z, w)) → f.0-0(f.0-1(x, y), f.0-1(z, w))
f.0-0(f.0-0(s.0(x), s.0(y)), f.0-1(z, w)) → f.0-0(f.0-0(x, y), f.0-1(z, w))
f.0-0(f.0-1(s.0(x), 0.), f.1-1(y, z)) → f.0-0(f.1-1(y, z), f.1-1(y, s.1(z)))
f.0-0(f.1-1(s.1(x), 0.), f.0-1(y, z)) → f.0-0(f.0-1(y, z), f.0-1(y, s.1(z)))
f.0-0(f.1-1(s.1(x), s.1(y)), f.0-1(z, w)) → f.0-0(f.1-1(x, y), f.0-1(z, w))
f.0-0(f.1-1(s.1(x), s.1(y)), f.0-0(z, w)) → f.0-0(f.1-1(x, y), f.0-0(z, w))
f.0-0(f.0-0(s.0(x), s.0(y)), f.1-1(z, w)) → f.0-0(f.0-0(x, y), f.1-1(z, w))
f.0-0(f.0-1(s.0(x), 0.), f.0-0(y, z)) → f.0-0(f.0-0(y, z), f.0-0(y, s.0(z)))
f.0-0(f.1-1(s.1(x), 0.), f.0-0(y, z)) → f.0-0(f.0-0(y, z), f.0-0(y, s.0(z)))
f.0-0(f.0-1(s.0(x), 0.), f.0-1(y, z)) → f.0-0(f.0-1(y, z), f.0-1(y, s.1(z)))
f.0-0(f.1-1(s.1(x), s.1(y)), f.1-1(z, w)) → f.0-0(f.1-1(x, y), f.1-1(z, w))
f.0-0(f.0-0(s.0(x), s.0(y)), f.0-0(z, w)) → f.0-0(f.0-0(x, y), f.0-0(z, w))
f.0-0(f.1-1(s.1(x), 0.), f.1-0(y, z)) → f.0-0(f.1-0(y, z), f.1-0(y, s.0(z)))
f.0-0(f.0-1(s.0(x), s.1(y)), f.0-0(z, w)) → f.0-0(f.0-1(x, y), f.0-0(z, w))
f.0-0(f.1-0(s.1(x), s.0(y)), f.1-0(z, w)) → f.0-0(f.1-0(x, y), f.1-0(z, w))
f.0-0(f.1-0(s.1(x), s.0(y)), f.0-1(z, w)) → f.0-0(f.1-0(x, y), f.0-1(z, w))
f.0-0(f.0-1(s.0(x), s.1(y)), f.1-0(z, w)) → f.0-0(f.0-1(x, y), f.1-0(z, w))
f.0-0(f.0-1(s.0(x), s.1(y)), f.1-1(z, w)) → f.0-0(f.0-1(x, y), f.1-1(z, w))
f.0-0(f.1-1(s.1(x), 0.), f.1-1(y, z)) → f.0-0(f.1-1(y, z), f.1-1(y, s.1(z)))
f.0-0(f.1-0(s.1(x), s.0(y)), f.0-0(z, w)) → f.0-0(f.1-0(x, y), f.0-0(z, w))
f.0-0(f.0-1(s.0(x), 0.), f.1-0(y, z)) → f.0-0(f.1-0(y, z), f.1-0(y, s.0(z)))
f.0-0(f.1-0(s.1(x), s.0(y)), f.1-1(z, w)) → f.0-0(f.1-0(x, y), f.1-1(z, w))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ SemLabProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesReductionPairsProof
↳ QDP
↳ SemLabProof2
F.0-0(f.1-1(s.1(s.1(y_0)), s.1(s.1(y_1))), f.0-1(x2, x3)) → F.0-0(f.1-1(s.1(y_0), s.1(y_1)), f.0-1(x2, x3))
f.0-0(f.0-0(s.0(x), s.0(y)), f.1-0(z, w)) → f.0-0(f.0-0(x, y), f.1-0(z, w))
f.0-0(f.1-1(s.1(x), s.1(y)), f.1-0(z, w)) → f.0-0(f.1-1(x, y), f.1-0(z, w))
f.0-0(f.0-1(s.0(x), s.1(y)), f.0-1(z, w)) → f.0-0(f.0-1(x, y), f.0-1(z, w))
f.0-0(f.0-0(s.0(x), s.0(y)), f.0-1(z, w)) → f.0-0(f.0-0(x, y), f.0-1(z, w))
f.0-0(f.0-1(s.0(x), 0.), f.1-1(y, z)) → f.0-0(f.1-1(y, z), f.1-1(y, s.1(z)))
f.0-0(f.1-1(s.1(x), 0.), f.0-1(y, z)) → f.0-0(f.0-1(y, z), f.0-1(y, s.1(z)))
f.0-0(f.1-1(s.1(x), s.1(y)), f.0-1(z, w)) → f.0-0(f.1-1(x, y), f.0-1(z, w))
f.0-0(f.1-1(s.1(x), s.1(y)), f.0-0(z, w)) → f.0-0(f.1-1(x, y), f.0-0(z, w))
f.0-0(f.0-0(s.0(x), s.0(y)), f.1-1(z, w)) → f.0-0(f.0-0(x, y), f.1-1(z, w))
f.0-0(f.0-1(s.0(x), 0.), f.0-0(y, z)) → f.0-0(f.0-0(y, z), f.0-0(y, s.0(z)))
f.0-0(f.1-1(s.1(x), 0.), f.0-0(y, z)) → f.0-0(f.0-0(y, z), f.0-0(y, s.0(z)))
f.0-0(f.0-1(s.0(x), 0.), f.0-1(y, z)) → f.0-0(f.0-1(y, z), f.0-1(y, s.1(z)))
f.0-0(f.1-1(s.1(x), s.1(y)), f.1-1(z, w)) → f.0-0(f.1-1(x, y), f.1-1(z, w))
f.0-0(f.0-0(s.0(x), s.0(y)), f.0-0(z, w)) → f.0-0(f.0-0(x, y), f.0-0(z, w))
f.0-0(f.1-1(s.1(x), 0.), f.1-0(y, z)) → f.0-0(f.1-0(y, z), f.1-0(y, s.0(z)))
f.0-0(f.0-1(s.0(x), s.1(y)), f.0-0(z, w)) → f.0-0(f.0-1(x, y), f.0-0(z, w))
f.0-0(f.1-0(s.1(x), s.0(y)), f.1-0(z, w)) → f.0-0(f.1-0(x, y), f.1-0(z, w))
f.0-0(f.1-0(s.1(x), s.0(y)), f.0-1(z, w)) → f.0-0(f.1-0(x, y), f.0-1(z, w))
f.0-0(f.0-1(s.0(x), s.1(y)), f.1-0(z, w)) → f.0-0(f.0-1(x, y), f.1-0(z, w))
f.0-0(f.0-1(s.0(x), s.1(y)), f.1-1(z, w)) → f.0-0(f.0-1(x, y), f.1-1(z, w))
f.0-0(f.1-1(s.1(x), 0.), f.1-1(y, z)) → f.0-0(f.1-1(y, z), f.1-1(y, s.1(z)))
f.0-0(f.1-0(s.1(x), s.0(y)), f.0-0(z, w)) → f.0-0(f.1-0(x, y), f.0-0(z, w))
f.0-0(f.0-1(s.0(x), 0.), f.1-0(y, z)) → f.0-0(f.1-0(y, z), f.1-0(y, s.0(z)))
f.0-0(f.1-0(s.1(x), s.0(y)), f.1-1(z, w)) → f.0-0(f.1-0(x, y), f.1-1(z, w))
POL(F.0-0(x1, x2)) = x1 + x2
POL(f.0-1(x1, x2)) = x1 + x2
POL(f.1-1(x1, x2)) = x1 + x2
POL(s.1(x1)) = x1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ SemLabProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesReductionPairsProof
↳ QDP
↳ RuleRemovalProof
↳ QDP
↳ SemLabProof2
F.0-0(f.1-1(s.1(s.1(y_0)), s.1(s.1(y_1))), f.0-1(x2, x3)) → F.0-0(f.1-1(s.1(y_0), s.1(y_1)), f.0-1(x2, x3))
F.0-0(f.1-1(s.1(s.1(y_0)), s.1(s.1(y_1))), f.0-1(x2, x3)) → F.0-0(f.1-1(s.1(y_0), s.1(y_1)), f.0-1(x2, x3))
POL(F.0-0(x1, x2)) = x1 + x2
POL(f.0-1(x1, x2)) = x1 + x2
POL(f.1-1(x1, x2)) = x1 + x2
POL(s.1(x1)) = 1 + x1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ SemLabProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesReductionPairsProof
↳ QDP
↳ RuleRemovalProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ SemLabProof2
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ SemLabProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ SemLabProof2
F.0-0(f.0-0(s.0(f.1-1(s.1(s.1(y_0)), s.1(0.))), s.0(x1)), f.1-1(x2, x3)) → F.0-0(f.1-1(s.1(s.1(y_0)), s.1(0.)), x1)
F.0-0(f.0-0(s.0(f.0-1(s.0(y_0), 0.)), s.0(f.0-0(s.0(y_1), s.0(y_2)))), f.1-1(x2, x3)) → F.0-0(f.0-1(s.0(y_0), 0.), f.0-0(s.0(y_1), s.0(y_2)))
F.0-0(f.0-0(s.0(f.1-1(s.1(y_0), s.1(y_1))), s.0(x1)), f.1-0(x2, x3)) → F.0-0(f.1-1(s.1(y_0), s.1(y_1)), x1)
F.0-0(f.0-0(s.0(f.0-1(s.0(y_0), 0.)), s.0(f.0-0(s.0(s.0(y_1)), s.0(s.0(y_2))))), f.1-0(x2, x3)) → F.0-0(f.0-1(s.0(y_0), 0.), f.0-0(s.0(s.0(y_1)), s.0(s.0(y_2))))
F.0-0(f.1-1(s.1(x0), 0.), f.0-0(s.0(s.0(y_0)), s.0(s.0(y_1)))) → F.0-0(f.0-0(s.0(s.0(y_0)), s.0(s.0(y_1))), f.0-0(s.0(s.0(y_0)), s.0(s.0(s.0(y_1)))))
F.0-0(f.0-1(s.0(s.0(y_0)), s.1(0.)), f.0-0(x2, x3)) → F.0-0(f.0-1(s.0(y_0), 0.), f.0-0(x2, x3))
F.0-0(f.0-0(s.0(f.0-1(s.0(y_0), 0.)), s.0(f.0-0(s.0(y_1), s.0(y_2)))), f.1-0(x2, x3)) → F.0-0(f.0-1(s.0(y_0), 0.), f.0-0(s.0(y_1), s.0(y_2)))
F.0-0(f.0-0(s.0(f.0-1(s.0(y_0), 0.)), s.0(f.0-0(s.0(y_1), s.0(y_2)))), f.0-0(x2, x3)) → F.0-0(f.0-1(s.0(y_0), 0.), f.0-0(s.0(y_1), s.0(y_2)))
F.0-0(f.0-0(s.0(f.0-1(s.0(y_0), s.1(y_1))), s.0(x1)), f.1-1(x2, x3)) → F.0-0(f.0-1(s.0(y_0), s.1(y_1)), x1)
F.0-0(f.0-0(s.0(s.0(y_0)), s.0(s.0(y_1))), f.0-1(x2, x3)) → F.0-0(f.0-0(s.0(y_0), s.0(y_1)), f.0-1(x2, x3))
F.0-0(f.0-0(s.0(f.0-1(s.0(s.0(y_0)), s.1(s.1(y_1)))), s.0(x1)), f.1-0(x2, x3)) → F.0-0(f.0-1(s.0(s.0(y_0)), s.1(s.1(y_1))), x1)
F.0-0(f.0-0(s.0(f.0-1(s.0(y_0), 0.)), s.0(f.0-0(s.0(y_1), s.0(y_2)))), f.0-1(x2, x3)) → F.0-0(f.0-1(s.0(y_0), 0.), f.0-0(s.0(y_1), s.0(y_2)))
F.0-0(f.0-0(s.0(f.0-0(s.0(s.0(y_0)), s.0(s.0(y_1)))), s.0(x1)), f.0-1(x2, x3)) → F.0-0(f.0-0(s.0(s.0(y_0)), s.0(s.0(y_1))), x1)
F.0-0(f.0-0(s.0(f.1-1(s.1(y_0), 0.)), s.0(f.0-0(s.0(s.0(y_1)), s.0(s.0(y_2))))), f.1-1(x2, x3)) → F.0-0(f.1-1(s.1(y_0), 0.), f.0-0(s.0(s.0(y_1)), s.0(s.0(y_2))))
F.0-0(f.1-1(s.1(s.1(y_0)), s.1(s.1(y_1))), f.0-0(x2, x3)) → F.0-0(f.1-1(s.1(y_0), s.1(y_1)), f.0-0(x2, x3))
F.0-0(f.0-0(s.0(f.0-1(s.0(y_0), s.1(y_1))), s.0(x1)), f.0-0(x2, x3)) → F.0-0(f.0-1(s.0(y_0), s.1(y_1)), x1)
F.0-0(f.0-1(s.0(x0), 0.), f.0-0(s.0(s.0(y_0)), s.0(s.0(y_1)))) → F.0-0(f.0-0(s.0(s.0(y_0)), s.0(s.0(y_1))), f.0-0(s.0(s.0(y_0)), s.0(s.0(s.0(y_1)))))
F.0-0(f.0-0(s.0(s.0(y_0)), s.0(s.0(y_1))), f.0-0(x2, x3)) → F.0-0(f.0-0(s.0(y_0), s.0(y_1)), f.0-0(x2, x3))
F.0-0(f.0-0(s.0(f.0-1(s.0(s.0(y_0)), s.1(0.))), s.0(x1)), f.1-1(x2, x3)) → F.0-0(f.0-1(s.0(s.0(y_0)), s.1(0.)), x1)
F.0-0(f.1-1(s.1(s.1(y_0)), s.1(0.)), f.0-0(x2, x3)) → F.0-0(f.1-1(s.1(y_0), 0.), f.0-0(x2, x3))
F.0-0(f.0-0(s.0(f.0-1(s.0(y_0), s.1(y_1))), s.0(x1)), f.0-1(x2, x3)) → F.0-0(f.0-1(s.0(y_0), s.1(y_1)), x1)
F.0-0(f.0-0(s.0(s.0(y_0)), s.0(s.0(y_1))), f.1-1(x2, x3)) → F.0-0(f.0-0(s.0(y_0), s.0(y_1)), f.1-1(x2, x3))
F.0-0(f.0-0(s.0(f.1-1(s.1(y_0), s.1(y_1))), s.0(x1)), f.0-0(x2, x3)) → F.0-0(f.1-1(s.1(y_0), s.1(y_1)), x1)
F.0-0(f.0-0(s.0(f.0-1(s.0(s.0(y_0)), s.1(s.1(y_1)))), s.0(x1)), f.1-1(x2, x3)) → F.0-0(f.0-1(s.0(s.0(y_0)), s.1(s.1(y_1))), x1)
F.0-0(f.0-0(s.0(f.0-1(s.0(s.0(y_0)), s.1(0.))), s.0(x1)), f.1-0(x2, x3)) → F.0-0(f.0-1(s.0(s.0(y_0)), s.1(0.)), x1)
F.0-0(f.0-0(s.0(f.0-0(s.0(y_0), s.0(y_1))), s.0(x1)), f.1-0(x2, x3)) → F.0-0(f.0-0(s.0(y_0), s.0(y_1)), x1)
F.0-0(f.0-0(s.0(f.1-1(s.1(s.1(y_0)), s.1(0.))), s.0(x1)), f.1-0(x2, x3)) → F.0-0(f.1-1(s.1(s.1(y_0)), s.1(0.)), x1)
F.0-0(f.0-1(s.0(x0), 0.), f.0-0(s.0(y_0), s.0(y_1))) → F.0-0(f.0-0(s.0(y_0), s.0(y_1)), f.0-0(s.0(y_0), s.0(s.0(y_1))))
F.0-0(f.0-0(s.0(f.0-1(s.0(y_0), 0.)), s.0(f.0-0(s.0(s.0(y_1)), s.0(s.0(y_2))))), f.1-1(x2, x3)) → F.0-0(f.0-1(s.0(y_0), 0.), f.0-0(s.0(s.0(y_1)), s.0(s.0(y_2))))
F.0-0(f.0-0(s.0(f.1-1(s.1(y_0), s.1(y_1))), s.0(x1)), f.0-1(x2, x3)) → F.0-0(f.1-1(s.1(y_0), s.1(y_1)), x1)
F.0-0(f.0-0(s.0(f.1-1(s.1(y_0), 0.)), s.0(f.0-0(s.0(y_1), s.0(y_2)))), f.0-0(x2, x3)) → F.0-0(f.1-1(s.1(y_0), 0.), f.0-0(s.0(y_1), s.0(y_2)))
F.0-0(f.0-0(s.0(f.1-1(s.1(s.1(y_0)), s.1(s.1(y_1)))), s.0(x1)), f.1-0(x2, x3)) → F.0-0(f.1-1(s.1(s.1(y_0)), s.1(s.1(y_1))), x1)
F.0-0(f.0-0(s.0(f.1-1(s.1(s.1(y_0)), s.1(s.1(y_1)))), s.0(x1)), f.0-1(x2, x3)) → F.0-0(f.1-1(s.1(s.1(y_0)), s.1(s.1(y_1))), x1)
F.0-0(f.0-0(s.0(f.1-1(s.1(y_0), 0.)), s.0(f.0-0(s.0(s.0(y_1)), s.0(s.0(y_2))))), f.0-1(x2, x3)) → F.0-0(f.1-1(s.1(y_0), 0.), f.0-0(s.0(s.0(y_1)), s.0(s.0(y_2))))
F.0-0(f.0-0(s.0(f.0-0(s.0(s.0(y_0)), s.0(s.0(y_1)))), s.0(x1)), f.0-0(x2, x3)) → F.0-0(f.0-0(s.0(s.0(y_0)), s.0(s.0(y_1))), x1)
F.0-0(f.0-0(s.0(f.1-1(s.1(s.1(y_0)), s.1(s.1(y_1)))), s.0(x1)), f.1-1(x2, x3)) → F.0-0(f.1-1(s.1(s.1(y_0)), s.1(s.1(y_1))), x1)
F.0-0(f.0-0(s.0(f.1-1(s.1(s.1(y_0)), s.1(0.))), s.0(x1)), f.0-0(x2, x3)) → F.0-0(f.1-1(s.1(s.1(y_0)), s.1(0.)), x1)
F.0-0(f.0-0(s.0(f.1-1(s.1(y_0), 0.)), s.0(f.0-0(s.0(y_1), s.0(y_2)))), f.1-1(x2, x3)) → F.0-0(f.1-1(s.1(y_0), 0.), f.0-0(s.0(y_1), s.0(y_2)))
F.0-0(f.0-0(s.0(f.0-0(s.0(y_0), s.0(y_1))), s.0(x1)), f.0-1(x2, x3)) → F.0-0(f.0-0(s.0(y_0), s.0(y_1)), x1)
F.0-0(f.0-0(s.0(f.0-1(s.0(y_0), s.1(y_1))), s.0(x1)), f.1-0(x2, x3)) → F.0-0(f.0-1(s.0(y_0), s.1(y_1)), x1)
F.0-0(f.0-0(s.0(f.0-1(s.0(s.0(y_0)), s.1(0.))), s.0(x1)), f.0-1(x2, x3)) → F.0-0(f.0-1(s.0(s.0(y_0)), s.1(0.)), x1)
F.0-0(f.0-0(s.0(s.0(y_0)), s.0(s.0(y_1))), f.1-0(x2, x3)) → F.0-0(f.0-0(s.0(y_0), s.0(y_1)), f.1-0(x2, x3))
F.0-0(f.0-0(s.0(f.0-0(s.0(s.0(y_0)), s.0(s.0(y_1)))), s.0(x1)), f.1-1(x2, x3)) → F.0-0(f.0-0(s.0(s.0(y_0)), s.0(s.0(y_1))), x1)
F.0-0(f.0-0(s.0(f.1-1(s.1(s.1(y_0)), s.1(0.))), s.0(x1)), f.0-1(x2, x3)) → F.0-0(f.1-1(s.1(s.1(y_0)), s.1(0.)), x1)
F.0-0(f.0-1(s.0(s.0(y_0)), s.1(s.1(y_1))), f.0-0(x2, x3)) → F.0-0(f.0-1(s.0(y_0), s.1(y_1)), f.0-0(x2, x3))
F.0-0(f.0-0(s.0(f.0-1(s.0(y_0), 0.)), s.0(f.0-0(s.0(s.0(y_1)), s.0(s.0(y_2))))), f.0-0(x2, x3)) → F.0-0(f.0-1(s.0(y_0), 0.), f.0-0(s.0(s.0(y_1)), s.0(s.0(y_2))))
F.0-0(f.0-0(s.0(f.0-1(s.0(s.0(y_0)), s.1(s.1(y_1)))), s.0(x1)), f.0-1(x2, x3)) → F.0-0(f.0-1(s.0(s.0(y_0)), s.1(s.1(y_1))), x1)
F.0-0(f.1-1(s.1(x0), 0.), f.0-0(s.0(y_0), s.0(y_1))) → F.0-0(f.0-0(s.0(y_0), s.0(y_1)), f.0-0(s.0(y_0), s.0(s.0(y_1))))
F.0-0(f.0-0(s.0(f.1-1(s.1(y_0), s.1(y_1))), s.0(x1)), f.1-1(x2, x3)) → F.0-0(f.1-1(s.1(y_0), s.1(y_1)), x1)
F.0-0(f.0-0(s.0(f.0-1(s.0(s.0(y_0)), s.1(0.))), s.0(x1)), f.0-0(x2, x3)) → F.0-0(f.0-1(s.0(s.0(y_0)), s.1(0.)), x1)
F.0-0(f.0-0(s.0(f.1-1(s.1(y_0), 0.)), s.0(f.0-0(s.0(s.0(y_1)), s.0(s.0(y_2))))), f.0-0(x2, x3)) → F.0-0(f.1-1(s.1(y_0), 0.), f.0-0(s.0(s.0(y_1)), s.0(s.0(y_2))))
F.0-0(f.0-0(s.0(f.1-1(s.1(y_0), 0.)), s.0(f.0-0(s.0(s.0(y_1)), s.0(s.0(y_2))))), f.1-0(x2, x3)) → F.0-0(f.1-1(s.1(y_0), 0.), f.0-0(s.0(s.0(y_1)), s.0(s.0(y_2))))
F.0-0(f.0-0(s.0(f.0-0(s.0(s.0(y_0)), s.0(s.0(y_1)))), s.0(x1)), f.1-0(x2, x3)) → F.0-0(f.0-0(s.0(s.0(y_0)), s.0(s.0(y_1))), x1)
F.0-0(f.0-0(s.0(f.0-1(s.0(y_0), 0.)), s.0(f.0-0(s.0(s.0(y_1)), s.0(s.0(y_2))))), f.0-1(x2, x3)) → F.0-0(f.0-1(s.0(y_0), 0.), f.0-0(s.0(s.0(y_1)), s.0(s.0(y_2))))
F.0-0(f.0-0(s.0(f.1-1(s.1(y_0), 0.)), s.0(f.0-0(s.0(y_1), s.0(y_2)))), f.1-0(x2, x3)) → F.0-0(f.1-1(s.1(y_0), 0.), f.0-0(s.0(y_1), s.0(y_2)))
F.0-0(f.0-0(s.0(f.0-1(s.0(s.0(y_0)), s.1(s.1(y_1)))), s.0(x1)), f.0-0(x2, x3)) → F.0-0(f.0-1(s.0(s.0(y_0)), s.1(s.1(y_1))), x1)
F.0-0(f.0-0(s.0(f.0-0(s.0(y_0), s.0(y_1))), s.0(x1)), f.0-0(x2, x3)) → F.0-0(f.0-0(s.0(y_0), s.0(y_1)), x1)
F.0-0(f.0-0(s.0(f.1-1(s.1(s.1(y_0)), s.1(s.1(y_1)))), s.0(x1)), f.0-0(x2, x3)) → F.0-0(f.1-1(s.1(s.1(y_0)), s.1(s.1(y_1))), x1)
F.0-0(f.0-0(s.0(f.1-1(s.1(y_0), 0.)), s.0(f.0-0(s.0(y_1), s.0(y_2)))), f.0-1(x2, x3)) → F.0-0(f.1-1(s.1(y_0), 0.), f.0-0(s.0(y_1), s.0(y_2)))
F.0-0(f.0-0(s.0(f.0-0(s.0(y_0), s.0(y_1))), s.0(x1)), f.1-1(x2, x3)) → F.0-0(f.0-0(s.0(y_0), s.0(y_1)), x1)
f.0-0(f.0-0(s.0(x), s.0(y)), f.1-0(z, w)) → f.0-0(f.0-0(x, y), f.1-0(z, w))
f.0-0(f.1-1(s.1(x), s.1(y)), f.1-0(z, w)) → f.0-0(f.1-1(x, y), f.1-0(z, w))
f.0-0(f.0-1(s.0(x), s.1(y)), f.0-1(z, w)) → f.0-0(f.0-1(x, y), f.0-1(z, w))
f.0-0(f.0-0(s.0(x), s.0(y)), f.0-1(z, w)) → f.0-0(f.0-0(x, y), f.0-1(z, w))
f.0-0(f.0-1(s.0(x), 0.), f.1-1(y, z)) → f.0-0(f.1-1(y, z), f.1-1(y, s.1(z)))
f.0-0(f.1-1(s.1(x), 0.), f.0-1(y, z)) → f.0-0(f.0-1(y, z), f.0-1(y, s.1(z)))
f.0-0(f.1-1(s.1(x), s.1(y)), f.0-1(z, w)) → f.0-0(f.1-1(x, y), f.0-1(z, w))
f.0-0(f.1-1(s.1(x), s.1(y)), f.0-0(z, w)) → f.0-0(f.1-1(x, y), f.0-0(z, w))
f.0-0(f.0-0(s.0(x), s.0(y)), f.1-1(z, w)) → f.0-0(f.0-0(x, y), f.1-1(z, w))
f.0-0(f.0-1(s.0(x), 0.), f.0-0(y, z)) → f.0-0(f.0-0(y, z), f.0-0(y, s.0(z)))
f.0-0(f.1-1(s.1(x), 0.), f.0-0(y, z)) → f.0-0(f.0-0(y, z), f.0-0(y, s.0(z)))
f.0-0(f.0-1(s.0(x), 0.), f.0-1(y, z)) → f.0-0(f.0-1(y, z), f.0-1(y, s.1(z)))
f.0-0(f.1-1(s.1(x), s.1(y)), f.1-1(z, w)) → f.0-0(f.1-1(x, y), f.1-1(z, w))
f.0-0(f.0-0(s.0(x), s.0(y)), f.0-0(z, w)) → f.0-0(f.0-0(x, y), f.0-0(z, w))
f.0-0(f.1-1(s.1(x), 0.), f.1-0(y, z)) → f.0-0(f.1-0(y, z), f.1-0(y, s.0(z)))
f.0-0(f.0-1(s.0(x), s.1(y)), f.0-0(z, w)) → f.0-0(f.0-1(x, y), f.0-0(z, w))
f.0-0(f.1-0(s.1(x), s.0(y)), f.1-0(z, w)) → f.0-0(f.1-0(x, y), f.1-0(z, w))
f.0-0(f.1-0(s.1(x), s.0(y)), f.0-1(z, w)) → f.0-0(f.1-0(x, y), f.0-1(z, w))
f.0-0(f.0-1(s.0(x), s.1(y)), f.1-0(z, w)) → f.0-0(f.0-1(x, y), f.1-0(z, w))
f.0-0(f.0-1(s.0(x), s.1(y)), f.1-1(z, w)) → f.0-0(f.0-1(x, y), f.1-1(z, w))
f.0-0(f.1-1(s.1(x), 0.), f.1-1(y, z)) → f.0-0(f.1-1(y, z), f.1-1(y, s.1(z)))
f.0-0(f.1-0(s.1(x), s.0(y)), f.0-0(z, w)) → f.0-0(f.1-0(x, y), f.0-0(z, w))
f.0-0(f.0-1(s.0(x), 0.), f.1-0(y, z)) → f.0-0(f.1-0(y, z), f.1-0(y, s.0(z)))
f.0-0(f.1-0(s.1(x), s.0(y)), f.1-1(z, w)) → f.0-0(f.1-0(x, y), f.1-1(z, w))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ SemLabProof
↳ SemLabProof2
↳ QDP
F(f(s(f(s(y_0), 0)), s(f(s(s(y_1)), s(s(y_2))))), f(x2, x3)) → F(f(s(y_0), 0), f(s(s(y_1)), s(s(y_2))))
F(f(s(x0), 0), f(s(y_0), s(y_1))) → F(f(s(y_0), s(y_1)), f(s(y_0), s(s(y_1))))
F(f(s(x0), 0), f(s(s(y_0)), s(0))) → F(f(s(s(y_0)), s(0)), f(s(s(y_0)), s(s(0))))
F(f(s(s(y_0)), s(0)), f(x2, x3)) → F(f(s(y_0), 0), f(x2, x3))
F(f(s(x0), 0), f(s(s(y_0)), s(s(y_1)))) → F(f(s(s(y_0)), s(s(y_1))), f(s(s(y_0)), s(s(s(y_1)))))
F(f(s(f(s(y_0), s(y_1))), s(x1)), f(x2, x3)) → F(f(s(y_0), s(y_1)), x1)
F(f(s(f(s(s(y_0)), s(s(y_1)))), s(x1)), f(x2, x3)) → F(f(s(s(y_0)), s(s(y_1))), x1)
F(f(s(f(s(s(y_0)), s(0))), s(x1)), f(x2, x3)) → F(f(s(s(y_0)), s(0)), x1)
F(f(s(s(y_0)), s(s(y_1))), f(x2, x3)) → F(f(s(y_0), s(y_1)), f(x2, x3))
F(f(s(f(s(y_0), 0)), s(f(s(y_1), s(y_2)))), f(x2, x3)) → F(f(s(y_0), 0), f(s(y_1), s(y_2)))
f(f(s(x), 0), f(y, z)) → f(f(y, z), f(y, s(z)))
f(f(s(x), s(y)), f(z, w)) → f(f(x, y), f(z, w))